Book XI · Proposition 13

XI.13

From the same point two straight lines cannot be set up at right angles to the same plane on the same side.Heath, 1908

Every step, checked

• the three points describe a planegiven
• no other line from the same point is at right angles to the planeby XI.13
• and each of those lines is on the same side as the firstby XI.13

What it needs, and what needs it

Needs: nothing earlier.

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.13", THEOREM, sample=samples3.three_in_space)
def prop_XI_13(a: Point3, b: Point3, c: Point3) -> Out:
    """Two perpendiculars cannot stand at one point on one side of a plane."""
    hypothesis("the three points describe a plane", not collinear3(a, b, c))
    surface = plane_through(a, b, c, "the given plane")
    normal = surface.normal()
    top = posit3(Point3(a.x + normal[0], a.y + normal[1], a.z + normal[2]), "D")
    line3(a, top, "the perpendicular")

    # The proposition denies a second one, so what is checked is the denial:
    # every other line drawn from A leans, and only the normal direction meets
    # the whole plane squarely.
    others = [Point3(top.x + (b.x - a.x) * Fraction(k, 4),
                     top.y + (b.y - a.y) * Fraction(k, 4),
                     top.z + (b.z - a.z) * Fraction(k, 4))
              for k in range(1, 5)]
    claim("no other line from the same point is at right angles to the plane",
          "XI.13",
          not any(_perpendicular_to_plane(Line3.through(a, other), surface)
                  for other in others))
    claim("and each of those lines is on the same side as the first", "XI.13",
          all(same_side_of_plane(other, top, surface) for other in others))
    return Out(perpendicular=Line3.through(a, top))