Book XI · Proposition 14

XI.14

Planes to which the same straight line is at right angles will be parallel.Heath, 1908

Every step, checked

• the three points describe a planegiven
• D is off that planegiven
• the one line is at right angles to both planesby XI.Def.3
• therefore the planes are parallelby XI.14
• and being two planes and not one, they nowhere meetby XI.Def.8

What it needs, and what needs it

Needs: nothing earlier.

Used by: XI.24 XI.29 XI.31 XI.32 XII.13

Rests on: XI.Def.3, 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.14", THEOREM, sample=samples3.plane_and_point)
def prop_XI_14(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Planes at right angles to the same line are parallel."""
    hypothesis("the three points describe a plane", not collinear3(a, b, c))
    hypothesis("D is off that plane", not coplanar(a, b, c, d))
    first = plane_through(a, b, c, "the first plane")
    normal = first.normal()
    step = vector_between(a, d)
    lifted = [posit3(Point3(p.x + step[0], p.y + step[1], p.z + step[2]), name)
              for p, name in zip((a, b, c), ("E", "F", "G"))]
    second = plane_through(*lifted, "the second plane")
    upright = line3(a, posit3(Point3(a.x + normal[0], a.y + normal[1],
                                     a.z + normal[2]), "H"), "the perpendicular")

    claim("the one line is at right angles to both planes", "XI.Def.3",
          _perpendicular_to_plane(upright, first)
          and _perpendicular_to_plane(upright, second))
    claim("therefore the planes are parallel", "XI.14",
          parallel_planes(first, second))
    claim("and being two planes and not one, they nowhere meet", "XI.Def.8",
          first != second)
    return Out(planes=(first, second))