Book XI · Proposition 35

XI.35

If there be two equal plane angles, and on their vertices there be set up elevated straight lines containing equal angles with the original straight lines respectively, if on the elevated straight lines points be taken at random and perpendiculars be drawn from them to the planes in which the original angles are, and if from the points so arising in the planes straight lines be joined to the vertices of the original angles, they will contain, with the elevated straight lines, equal angles.Heath, 1908

Every step, checked

• the elevated line is out of the plane of the given anglegiven
• the second angle's arms have two distinct endsgiven
• the elevated line is not itself at right angles to the plane, so there is a join from the foot to the vertexgiven
• no two of the three angles are together a straight anglegiven
• the two plane angles are equalby I.Def.8
• and the elevated lines contain equal angles with their sidesby XI.26
• therefore the elevated lines contain equal angles with the joinsby XI.35

What it needs, and what needs it

Needs: XI.11 XI.26

Rests on: I.Def.8, XI.Def.11, XI.Def.3, XI.Def.7

Depth: 2 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 plane (×2)solid

The proposition as code

@proposition("XI.35", THEOREM, sample=samples3.two_corners)
def prop_XI_35(o: Point3, a: Point3, b: Point3, c: Point3,
               d: Point3, e: Point3, f: Point3, g: Point3) -> Out:
    """Two equal plane angles, with elevated lines making equal angles with
    their sides: the elevated lines make equal angles with the joins from the
    feet of the perpendiculars."""
    hypothesis("the elevated line is out of the plane of the given angle",
               not coplanar(o, a, b, c))
    hypothesis("the second angle's arms have two distinct ends", d != e)
    for arm in (a, b, c):
        line3(o, arm)

    base = plane_through(o, a, b, "the plane of the given angle")
    foot = posit3(_foot_on_plane(c, base), "L")
    hypothesis("the elevated line is not itself at right angles to the plane, "
               "so there is a join from the foot to the vertex", o != foot)
    line3(c, foot, "the perpendicular")
    line3(o, foot, "the join from the foot")
    because(prop_XI_11, o, a, b, c)

    # The second figure is set up from the angles alone, by XI.26's frame: the
    # plane angle and the two the elevated line makes with its sides. Nothing
    # of the first figure's coordinates crosses over, so the equality claimed
    # at the end is a conclusion and not a restatement.
    flat = angle_at3(a, o, b)
    with_first, with_second = angle_at3(a, o, c), angle_at3(b, o, c)
    hypothesis("no two of the three angles are together a straight angle",
               all(sign(1 - angle.cos * angle.cos) > 0
                   for angle in (flat, with_first, with_second)),
               guard=True)
    arms = tuple(posit3(point, name) for point, name in
                 zip(_arms_making(d, vector_between(d, e),
                                  (flat, with_second, with_first)), ("P", "Q", "M")))
    for arm in arms:
        line3(d, arm)
    second_base = plane_through(d, arms[0], arms[1], "the plane of the second angle")
    second_foot = posit3(_foot_on_plane(arms[2], second_base), "N")
    line3(arms[2], second_foot, "the second perpendicular")
    line3(d, second_foot, "the second join")

    claim("the two plane angles are equal", "I.Def.8",
          angle_at3(arms[0], d, arms[1]) == flat)
    claim("and the elevated lines contain equal angles with their sides", "XI.26",
          angle_at3(arms[0], d, arms[2]) == with_first
          and angle_at3(arms[1], d, arms[2]) == with_second)
    claim("therefore the elevated lines contain equal angles with the joins",
          "XI.35",
          angle_at3(c, o, foot) == angle_at3(arms[2], d, second_foot))
    return Out(feet=(foot, second_foot),
               angles=(angle_at3(c, o, foot), angle_at3(arms[2], d, second_foot)))