Book XI · Proposition 18

XI.18

If a straight line be at right angles to any plane, all the planes through it will also be at right angles to the same plane.Heath, 1908

Every step, checked

• the three points describe a planegiven
• D is off that planegiven
• the line is at right angles to the planegiven
• each of those planes holds the whole perpendicularby XI.Def.7
• and each is at right angles to the given planeby XI.18

What it needs, and what needs it

Needs: nothing earlier.

Rests on: XI.Def.7

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

The proposition as code

@proposition("XI.18", THEOREM, sample=samples3.plane_and_point)
def prop_XI_18(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Every plane through a perpendicular is perpendicular to the same plane."""
    hypothesis("the three points describe a plane", not collinear3(a, b, c))
    hypothesis("D is off that plane", not coplanar(a, b, c, d))
    surface = plane_through(a, b, c, "the given plane")
    normal = surface.normal()
    top = posit3(Point3(a.x + normal[0], a.y + normal[1], a.z + normal[2]), "H")
    upright = line3(a, top, "the perpendicular")
    hypothesis("the line is at right angles to the plane",
               _perpendicular_to_plane(upright, surface))

    through = [plane_through(a, top, point, label)
               for point, label in ((b, "the plane through B"),
                                    (c, "the plane through C"))]
    claim("each of those planes holds the whole perpendicular", "XI.Def.7",
          all(on_plane(a, plane) and on_plane(top, plane) for plane in through))
    claim("and each is at right angles to the given plane", "XI.18",
          all(dot3(plane.normal(), normal) == 0 for plane in through))
    return Out(planes=tuple(through))