Book VI · Proposition 32

VI.32

If two triangles having two sides proportional to two sides be placed together at one angle so that their corresponding sides are also parallel, the remaining sides of the triangles will be in a straight line.Heath, 1908
ABDEF
5 lines and circles drawn, of which 3 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.14 I.33

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4, Post.5

Depth: 11 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "VI.32",
    THEOREM,
    sample=_parallelogram_with_similar_corner,
)
def prop_VI_32(a: Point, b: Point, d: Point, part) -> Out:
    """Two similar triangles set together at a corner, with sides parallel."""
    hypothesis("the figure is genuine", not collinear(a, b, d), guard=True)
    hypothesis("the division is a proper one", sign(part) > 0 and sign(1 - part) > 0, guard=True)

    # Two triangles sharing the vertex A, the second the first scaled about it,
    # so corresponding sides are parallel and the outer sides fall in a line.
    e = posit(Point(a.x + (b.x - a.x) + (d.x - a.x), a.y + (b.y - a.y) + (d.y - a.y)), "E")
    far = posit(Point(a.x - part * (b.x - a.x), a.y - part * (b.y - a.y)), "F")
    outline(b, a, d)
    outline(d, e, close=False)
    line(far, b, "the side FB")

    # I.33 reads its alternate angles off one diagonal, and which pair those
    # are depends on the way round the two equal sides were named: AB with ED,
    # taken in that order, is the pair whose joins this figure makes.
    because(prop_I_33, a, b, e, d)
    # FA and AB stand on opposite sides of A and make two right angles together,
    # which is I.14's condition for their being one straight line.
    because(prop_I_14, far, a, b, d)

    claim("the corresponding sides are parallel", "I.33",
          parallel(Line.through(a, b), Line.through(d, e)))
    claim("so the remaining sides fall in one straight line", "I.14",
          collinear(far, a, b))
    return Out()