Book XI · Proposition 9

XI.9

Straight lines which are parallel to the same straight line and are not in the same plane with it are also parallel to one another.Heath, 1908

Every step, checked

• the second is parallel to the firstgiven
• they are distinct linesgiven
• the third is parallel to the first as wellgiven
• the third is out of the plane of the first twogiven
• the second and third are parallel to one anotherby XI.9

What it needs, and what needs it

Needs: nothing earlier.

Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

• a plane is described, and XI Def. 1-2; no postulate describes a planesolid

The proposition as code

@proposition(
    "XI.9",
    THEOREM,
    sample=samples3.parallel_lines3,
)
def prop_XI_9(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Lines parallel to the same line, and not in one plane with it, are
    parallel to one another."""
    middle = Line3.through(a, b)
    second = Line3.through(c, d)
    hypothesis("the second is parallel to the first", _parallel3(middle, second))
    hypothesis("they are distinct lines", not middle.holds(c))
    step = middle.direction()
    # The third parallel must be out of the plane the first two lie in, which is
    # the whole point: lift it along that plane's normal, so it is off the plane
    # by construction rather than by hoping the sampler put it there.
    up = plane_through(a, b, c).normal()
    away = posit3(Point3(c.x + up[0], c.y + up[1], c.z + up[2]), "E")
    third = line3(away, posit3(Point3(away.x + step[0], away.y + step[1],
                                      away.z + step[2]), "F"), "the third parallel")
    line3(a, b)
    line3(c, d)

    hypothesis("the third is parallel to the first as well", _parallel3(middle, third))
    # Two lines of one direction always lie in some plane together, so Euclid's
    # "not in the same plane with it" cannot mean that pair: it means the third
    # is out of the plane the first two already determine, which is the case his
    # proof is about and the only one that needs proving.
    hypothesis("the third is out of the plane of the first two",
               not coplanar(a, b, c, away))
    claim("the second and third are parallel to one another", "XI.9",
          _parallel3(second, third))
    return Out(lines=(middle, second, third))