Book XI · Proposition 19

XI.19

If two planes which cut one another be at right angles to any plane, their common section 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
• both are at right angles to the given planegiven
• they are two planes and not onegiven
• their common section is a straight lineby XI.3
• and it is at right angles to the given planeby XI.19

What it needs, and what needs it

Needs: XI.3

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

What it takes on trust

• a plane-plane intersection is used, though no postulate asserts that two planes meetcontinuity
• a plane is described, and XI Def. 1-2; no postulate describes a plane (×3)solid

The proposition as code

@proposition("XI.19", THEOREM, sample=samples3.plane_and_point)
def prop_XI_19(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Two planes at right angles to a third cut it in a perpendicular line."""
    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")
    first = plane_through(a, top, b, "the first plane")
    second = plane_through(a, top, c, "the second")
    hypothesis("both are at right angles to the given plane",
               dot3(first.normal(), normal) == 0
               and dot3(second.normal(), normal) == 0)
    hypothesis("they are two planes and not one", first != second)

    section = meet_planes(first, second)
    claim("their common section is a straight line", "XI.3",
          isinstance(section, Line3))
    claim("and it is at right angles to the given plane", "XI.19",
          _perpendicular_to_plane(section, surface))
    return Out(section=section)