Book XI · Proposition 6

XI.6

If two straight lines be at right angles to the same plane, the straight lines will be parallel.Heath, 1908

Every step, checked

• the three points describe a planegiven
• D is off that planegiven
• both are at right angles to the planeby XI.Def.3
• therefore they are parallelby XI.6
• and being distinct lines, they never meetby XI.Def.8

What it needs, and what needs it

Needs: nothing earlier.

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 planesolid

The proposition as code

@proposition(
    "XI.6",
    THEOREM,
    sample=samples3.plane_and_point,
)
def prop_XI_6(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Two lines at right angles to the same plane 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))
    surface = plane_through(a, b, c, "the plane")
    normal = surface.normal()

    # Two uprights, one at A and one at B: both along the normal, which is what
    # being at right angles to the plane means.
    first_top = posit3(Point3(a.x + normal[0], a.y + normal[1], a.z + normal[2]), "E")
    second_top = posit3(Point3(b.x + normal[0], b.y + normal[1], b.z + normal[2]), "F")
    first = line3(a, first_top, "the upright at A")
    second = line3(b, second_top, "the upright at B")

    claim("both are at right angles to the plane", "XI.Def.3",
          _perpendicular_to_plane(first, surface)
          and _perpendicular_to_plane(second, surface))
    claim("therefore they are parallel", "XI.6", _parallel3(first, second))
    claim("and being distinct lines, they never meet", "XI.Def.8",
          not first.holds(b))
    return Out(first=first, second=second)