Book XI · Proposition 15

XI.15

If two straight lines meeting one another be parallel to two straight lines meeting one another, not being in the same plane, the planes through them are parallel.Heath, 1908

Every step, checked

• the arms are not in one planegiven
• neither pair is in a straight linegiven
• the two pairs are not in one planegiven
• the arms are parallel, each to eachby XI.Def.8
• so the planes through them are parallelby XI.15

What it needs, and what needs it

Needs: nothing earlier.

Used by: XI.25

Rests on: XI.Def.8

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 plane (×2)solid

The proposition as code

@proposition("XI.15", THEOREM, sample=samples3.tetrahedron)
def prop_XI_15(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """Two pairs of meeting lines, parallel each to each, lie in parallel planes."""
    hypothesis("the arms are not in one plane", not coplanar(o, a, b, c))
    hypothesis("neither pair is in a straight line", not collinear3(o, a, b))
    step = vector_between(o, c)
    away = posit3(Point3(o.x + step[0], o.y + step[1], o.z + step[2]), "D")
    far_a = posit3(Point3(a.x + step[0], a.y + step[1], a.z + step[2]), "E")
    far_b = posit3(Point3(b.x + step[0], b.y + step[1], b.z + step[2]), "F")
    for pair in ((o, a), (o, b), (away, far_a), (away, far_b)):
        line3(*pair)

    first = plane_through(o, a, b, "the plane of the first pair")
    second = plane_through(away, far_a, far_b, "the plane of the second")
    hypothesis("the two pairs are not in one plane", first != second)

    claim("the arms are parallel, each to each", "XI.Def.8",
          _parallel3(Line3.through(o, a), Line3.through(away, far_a))
          and _parallel3(Line3.through(o, b), Line3.through(away, far_b)))
    claim("so the planes through them are parallel", "XI.15",
          parallel_planes(first, second))
    return Out(planes=(first, second))