Book XI · Proposition 11

XI.11

From a given elevated point to draw a straight line perpendicular to a given plane.Heath, 1908

Every step, checked

• the three points describe a planegiven
• D is elevated above that planegiven
• the foot lies in the given planeby XI.Def.7
• and the line drawn is at right angles to the planeby XI.11
• so it is at right angles to every line of the plane through the footby XI.Def.3

What it needs, and what needs it

Needs: nothing earlier.

Used by: XI.35

Rests on: XI.Def.3, XI.Def.7

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.11", CONSTRUCTION, sample=samples3.plane_and_point)
def prop_XI_11(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """From an elevated point, draw a line perpendicular to a given plane."""
    hypothesis("the three points describe a plane", not collinear3(a, b, c))
    hypothesis("D is elevated above that plane", not coplanar(a, b, c, d))
    surface = plane_through(a, b, c, "the given plane")
    foot = posit3(_foot_on_plane(d, surface), "F")
    dropped = line3(d, foot, "the perpendicular")

    claim("the foot lies in the given plane", "XI.Def.7", on_plane(foot, surface))
    claim("and the line drawn is at right angles to the plane", "XI.11",
          _perpendicular_to_plane(dropped, surface))
    claim("so it is at right angles to every line of the plane through the foot",
          "XI.Def.3",
          all(dot3(vector_between(d, foot), vector_between(foot, point)) == 0
              for point in (a, b, c) if point != foot))
    return Out(perpendicular=dropped, foot=foot)