Book XI · Proposition 4

XI.4

If a straight line be set up at right angles to two straight lines which cut one another, at their common point of section, it will also be at right angles to the plane through them.Heath, 1908

Every step, checked

• OA and OB cut one another at Ogiven
• OC is at right angles to bothgiven
• OC is at right angles to every straight line of the plane meeting itby XI.Def.3
• so OC is at right angles to the plane itselfby XI.4

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.4",
    THEOREM,
    sample=samples3.right_angled_at_origin,
)
def prop_XI_4(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """A line at right angles to two lines that cut it is at right angles to
    their plane."""
    hypothesis("OA and OB cut one another at O", not collinear3(o, a, b))
    hypothesis("OC is at right angles to both",
               dot3(vector_between(o, c), vector_between(o, a)) == 0
               and dot3(vector_between(o, c), vector_between(o, b)) == 0)
    surface = plane_through(o, a, b, "the plane of OA and OB")
    upright = line3(o, c, "the line set up at right angles")
    line3(o, a)
    line3(o, b)

    # "At right angles to the plane" is Definition XI.3: at right angles to
    # every straight line of the plane that meets it. Checking a spread of them
    # is checking the definition rather than a convenient consequence.
    through = [Point3(o.x + (a.x - o.x) * Fraction(k, 3) + (b.x - o.x) * Fraction(m, 3),
                      o.y + (a.y - o.y) * Fraction(k, 3) + (b.y - o.y) * Fraction(m, 3),
                      o.z + (a.z - o.z) * Fraction(k, 3) + (b.z - o.z) * Fraction(m, 3))
               for k in range(-3, 4) for m in range(-3, 4)]
    claim("OC is at right angles to every straight line of the plane meeting it",
          "XI.Def.3",
          all(dot3(vector_between(o, c), vector_between(o, point)) == 0
              for point in through if point != o))
    claim("so OC is at right angles to the plane itself", "XI.4",
          _perpendicular_to_plane(upright, surface))
    return Out(plane=surface, upright=upright)