Book XI · Proposition 28

XI.28

If a parallelepipedal solid be cut by a plane through the diagonals of the opposite planes, the solid will be bisected by the plane.Heath, 1908

Every step, checked

• the three arms are not in one planegiven
• the plane is carried through the diagonals of the opposite facesby XI.3
• the two prisms it makes are equal to one anotherby I.34
• so the solid is bisected by the planeby XI.28

What it needs, and what needs it

Needs: I.34 XI.3

Used by: XI.39

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

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

What it takes on trust

• a plane is described, and XI Def. 1-2; no postulate describes a planesolid

The proposition as code

@proposition("XI.28", THEOREM, sample=samples3.corner_and_arms)
def prop_XI_28(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """A parallelepiped cut by a plane through the diagonals of the opposite
    faces is bisected by that plane."""
    hypothesis("the three arms are not in one plane", not coplanar(o, a, b, c))
    solid = _built(parallelepiped(o, a, b, c, "the solid"))
    whole = content(solid)
    across = vector_between(o, c)

    near, far = solid.vertices[2], solid.vertices[6]
    line3(o, near, "the diagonal of the base")
    line3(solid.vertices[4], far, "the diagonal of the opposite face")
    cutter = plane_through(o, near, far, "the cutting plane")

    first = _built(prism((o, a, near), across, "the first prism"))
    second = _built(prism((o, near, b), across, "the second prism"))

    claim("the plane is carried through the diagonals of the opposite faces",
          "XI.3",
          on_plane(o, cutter) and on_plane(near, cutter)
          and on_plane(solid.vertices[4], cutter) and on_plane(far, cutter))
    claim("the two prisms it makes are equal to one another", "I.34",
          content(first) == content(second))
    claim("so the solid is bisected by the plane", "XI.28",
          content(first) + content(second) == whole
          and 2 * content(first) == whole)
    return Out(prisms=(first, second), plane=cutter)