Book VI · Proposition 20

VI.20

Similar polygons are divided into similar triangles, and into triangles equal in multitude and in the same ratio as the wholes, and the polygon has to the polygon a ratio duplicate of that which the corresponding side has to the corresponding side.Heath, 1908

The general form of Pythagoras' area law, and what VI.31 leans on: areas of similar figures go as the squares on their sides, whatever the figures are.

Every step, checked

• the polygons are similargiven
• neither is degenerategiven
• the polygons divide into triangles equal in multitudeby VI.Def.1
• and the triangles are similar, each to its fellowby VI.6, VI.4
• each triangle is to its fellow as the whole polygon is to the wholeby V.12
• similar triangles are to one another in the duplicate ratio of their corresponding sidesby VI.19
• therefore the polygon has to the polygon the duplicate ratio of the corresponding sidesby VI.19, V.12

What it needs, and what needs it

Needs: V.12 VI.4 VI.6 VI.19

Used by: VI.22 VI.31

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×2)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×2)continuity

The proposition as code

@proposition(
    "VI.20",
    THEOREM,
    sample=_similar_polygons,
    note="The general form of Pythagoras' area law, and what VI.31 leans on: "
    "areas of similar figures go as the squares on their sides, whatever the figures are.",
)
def prop_VI_20(
    a: Point, b: Point, c: Point, d: Point,
    p: Point, q: Point, r: Point, s: Point,
) -> Out:
    """ABCD and PQRS are similar; each is cut into triangles from a vertex."""
    first, second = [a, b, c, d], [p, q, r, s]

    # Similarity of polygons, said without angles: every distance between
    # corresponding vertices stands in one ratio. For a quadrilateral that is
    # the four sides and the two diagonals, which fix the shape.
    def in_one_ratio(i: int, j: int) -> bool:
        return (len2(first[i], first[j]) * len2(second[0], second[1])
                == len2(second[i], second[j]) * len2(first[0], first[1]))

    hypothesis("the polygons are similar",
               all(in_one_ratio(i, j) for i in range(4) for j in range(i + 1, 4)))
    hypothesis("neither is degenerate", not collinear(a, b, c) and not collinear(a, c, d))

    outline(*first)
    outline(*second)
    line(a, c, "the diameter dividing ABCD")
    line(p, r, "and the corresponding diameter of PQRS")

    # Fan each polygon into triangles from its first vertex, as Euclid does.
    def fan(vertices):
        return [(vertices[0], vertices[i], vertices[i + 1]) for i in range(1, len(vertices) - 1)]

    cut_first, cut_second = fan(first), fan(second)
    whole_first, whole_second = _area(*first), _area(*second)

    claim("the polygons divide into triangles equal in multitude", "VI.Def.1",
          len(cut_first) == len(cut_second))
    claim("and the triangles are similar, each to its fellow", ["VI.6", "VI.4"],
          all(similar(one, other) for one, other in zip(cut_first, cut_second)))
    claim("each triangle is to its fellow as the whole polygon is to the whole", "V.12",
          all(_area(*one) * whole_second == _area(*other) * whole_first
              for one, other in zip(cut_first, cut_second)))
    because(prop_VI_19, *cut_first[0], *cut_second[0])
    because(prop_VI_4, *cut_first[0], *cut_second[0])
    because(prop_VI_6, *cut_first[0], *cut_second[0])

    claim("similar triangles are to one another in the duplicate ratio of their "
          "corresponding sides", "VI.19",
          all(_area(*one) * len2(second[0], second[1])
              == _area(*other) * len2(first[0], first[1])
              for one, other in zip(cut_first, cut_second)))
    claim("therefore the polygon has to the polygon the duplicate ratio of the "
          "corresponding sides", ["VI.19", "V.12"],
          whole_first * len2(p, q) == whole_second * len2(a, b))
    return Out(triangles=(cut_first, cut_second))