Book I · Proposition 30

I.30

Straight lines parallel to the same straight line are also parallel to one another.Heath, 1908

Every step, checked

• AB is parallel to CDgiven
• EF is parallel to CDgiven
• a transversal makes equal alternate angles with each, so AB is parallel to EFby I.29

What it needs, and what needs it

Needs: I.29

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

Depth: 3 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(
    "I.30",
    THEOREM,
    sample=_three_parallels,
)
def prop_I_30(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    first, second, third = line(a, b, "AB"), line(c, d, "CD"), line(e, f, "EF")
    hypothesis("AB is parallel to CD", parallel(first, second))
    hypothesis("EF is parallel to CD", parallel(third, second))

    # One transversal across all three, and I.29 read off it twice. Alternate
    # angles lie on opposite sides of the transversal, so each line is named by
    # the pair of points either side of where it is crossed, in that order.
    transversal = Line.through(a, f)
    crossing = meet_one(transversal, second)

    def straddling(at: Point, along: Point, from_: Point) -> tuple:
        step = (along.x - from_.x, along.y - from_.y)
        near = Point(at.x + step[0], at.y + step[1])
        far = Point(at.x - step[0], at.y - step[1])
        return (near, far) if transversal.side_of(near) > 0 else (far, near)

    up_ab, down_ab = straddling(a, b, a)
    up_cd, down_cd = straddling(crossing, d, c)
    up_ef, down_ef = straddling(f, f, e)
    because(prop_I_29, up_ab, down_ab, up_cd, down_cd, a, crossing)
    because(prop_I_29, up_cd, down_cd, up_ef, down_ef, crossing, f)

    claim("a transversal makes equal alternate angles with each, so AB is parallel to EF",
          "I.29", parallel(first, third))
    return Out()