Book XI · Proposition 17

XI.17

If two straight lines be cut by parallel planes, they will be cut in the same ratios.Heath, 1908

Every step, checked

• the three points describe a planegiven
• D is off that planegiven
• the three planes are parallelgiven
• each line is cut by the middle planeby XI.Def.7
• and the two are cut in the same ratioby XI.17

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 line-plane intersection is used, though no postulate asserts that a line meets a plane (×2)continuity
• a plane is described, and XI Def. 1-2; no postulate describes a plane (×3)solid

The proposition as code

@proposition("XI.17", THEOREM, sample=samples3.plane_and_point)
def prop_XI_17(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Two straight lines cut by parallel planes are cut in the same ratios."""
    hypothesis("the three points describe a plane", not collinear3(a, b, c))
    hypothesis("D is off that plane", not coplanar(a, b, c, d))
    step = vector_between(a, d)
    first = plane_through(a, b, c, "the first plane")
    lifted = [posit3(Point3(p.x + step[0], p.y + step[1], p.z + step[2]), name)
              for p, name in zip((a, b, c), ("E", "F", "G"))]
    second = plane_through(*lifted, "the second, parallel to it")
    # A third plane parallel to both, cutting each line partway along.
    half = Fraction(1, 2)
    middle = [posit3(Point3(p.x + half * step[0], p.y + half * step[1],
                            p.z + half * step[2]), name)
              for p, name in zip((a, b, c), ("K", "L", "M"))]
    third = plane_through(*middle, "the plane between them")
    hypothesis("the three planes are parallel",
               parallel_planes(first, second) and parallel_planes(first, third))

    # Two lines cut by all three: A to its lift, and B to its lift.
    one = line3(a, lifted[0], "the first line")
    other = line3(b, lifted[1], "the second line")
    here = meet_line_plane(one, third)
    there = meet_line_plane(other, third)

    claim("each line is cut by the middle plane", "XI.Def.7",
          on_plane(here, third) and on_plane(there, third))
    # Ratios of lengths along a line are ratios of squared lengths crosswise,
    # which keeps the comparison exact and takes no root.
    claim("and the two are cut in the same ratio", "XI.17",
          len2(a, here) * len2(there, lifted[1]) == len2(here, lifted[0]) * len2(b, there))
    return Out(sections=(here, there))