Book XI · Proposition 8

XI.8

If two straight lines be parallel, and one of them be at right angles to any plane, the remaining one 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 two are parallelgiven
• the first is at right angles to the planeby XI.Def.3
• so the second is at right angles to the same planeby XI.8

What it needs, and what needs it

Needs: nothing earlier.

Rests on: XI.Def.3

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.8",
    THEOREM,
    sample=samples3.plane_and_point,
)
def prop_XI_8(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """If one of two parallels is at right angles to a plane, so is the other."""
    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()
    top = posit3(Point3(a.x + normal[0], a.y + normal[1], a.z + normal[2]), "E")
    upright = line3(a, top, "the upright at A")
    alongside = line3(b, posit3(Point3(b.x + normal[0], b.y + normal[1],
                                       b.z + normal[2]), "F"), "its parallel")

    hypothesis("the two are parallel", _parallel3(upright, alongside))
    claim("the first is at right angles to the plane", "XI.Def.3",
          _perpendicular_to_plane(upright, surface))
    claim("so the second is at right angles to the same plane", "XI.8",
          _perpendicular_to_plane(alongside, surface))
    return Out(upright=upright, alongside=alongside)