Book XI · Proposition 5

XI.5

If a straight line be set up at right angles to three straight lines which meet one another, at their common point of section, the three straight lines are in one plane.Heath, 1908

Every step, checked

• OA and OB are not in a straight linegiven
• the line is at right angles to all threegiven
• the third line is at right angles to OC as wellby XI.Def.3
• and the three lines are in one planeby XI.5

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.5",
    THEOREM,
    sample=samples3.right_angled_at_origin,
)
def prop_XI_5(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """A line at right angles to three concurrent lines puts those three in one
    plane."""
    hypothesis("OA and OB are not in a straight line", not collinear3(o, a, b))
    hypothesis("the line is at right angles to all three",
               dot3(vector_between(o, c), vector_between(o, a)) == 0
               and dot3(vector_between(o, c), vector_between(o, b)) == 0)
    # The third line of Euclid's figure is any other perpendicular to OC at O,
    # and the proposition is that it cannot escape the plane of the first two.
    third = posit3(Point3(o.x + (a.x - o.x) + (b.x - o.x),
                          o.y + (a.y - o.y) + (b.y - o.y),
                          o.z + (a.z - o.z) + (b.z - o.z)), "D")
    surface = plane_through(o, a, b, "the plane of the three")
    line3(o, c, "the perpendicular")

    claim("the third line is at right angles to OC as well", "XI.Def.3",
          dot3(vector_between(o, c), vector_between(o, third)) == 0)
    claim("and the three lines are in one plane", "XI.5",
          on_plane(a, surface) and on_plane(b, surface) and on_plane(third, surface))
    return Out(plane=surface)