Book XI · Proposition 12

XI.12

To set up a straight line at right angles to a given plane from a given point in it.Heath, 1908

Every step, checked

• the three points describe a planegiven
• the line stands on the given point of the planeby XI.Def.7
• and it is at right angles to the planeby XI.12

What it needs, and what needs it

Needs: nothing earlier.

Rests on: 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.12", CONSTRUCTION, sample=samples3.three_in_space)
def prop_XI_12(a: Point3, b: Point3, c: Point3) -> Out:
    """Set up a line at right angles to a plane, from a point in it."""
    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")
    upright = line3(a, top, "the line set up")

    claim("the line stands on the given point of the plane", "XI.Def.7",
          on_plane(a, surface) and not on_plane(top, surface))
    claim("and it is at right angles to the plane", "XI.12",
          _perpendicular_to_plane(upright, surface))
    return Out(upright=upright)