Book XI · Proposition 30

XI.30

Parallelepipedal solids which are on the same base and of the same height, and in which the extremities of the sides which stand up are not on the same straight lines, are equal to one another.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: XI.29

Used by: XI.31

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

Depth: 13 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("XI.30", THEOREM, sample=samples3.corner_and_arms)
def prop_XI_30(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """Parallelepipeds on the same base and of the same height, whose standing
    sides do not end on the same straight lines, are equal."""
    hypothesis("the three arms are not in one plane", not coplanar(o, a, b, c))
    first = _built(parallelepiped(o, a, b, c, "the first solid"))
    # Slid across both arms of the base, so the top runs in neither of the lines
    # XI.29 leaves it in: the same plane is reached by a different route.
    one, other = vector_between(o, a), vector_between(o, b)
    leaned = posit3(Point3(c.x + one[0] + other[0], c.y + one[1] + other[1],
                           c.z + one[2] + other[2]), "M")
    second = _built(parallelepiped(o, a, b, leaned, "the second solid"))

    because(prop_XI_29, o, a, b, c)

    claim("the two solids stand on the same base and reach the same plane",
          "XI.29",
          _same_figure(first.face_points(0), second.face_points(0))
          and second.face_plane(1) == first.face_plane(1))
    claim("the tops do not lie in the same straight lines", "XI.Def.10",
          not on_line3(leaned, Line3.through(c, first.vertices[5]))
          and not on_line3(leaned, Line3.through(c, first.vertices[7])))
    claim("and the solids are equal to one another", "XI.30",
          content(first) == content(second))
    return Out(solids=(first, second))