Dear Self,
For future reference: Of course, this is outlined very nicely in Coxeter's
Introduction to Geometry, (second edition), but as always the best way to learn math is to re-work it. Here, a proof-sketch without pictures.
By
sphere S signify the level set---in some vector space
V---of some positive-definite quadratic form; or equivalently the orbit of a generic point under the orthogonal group of the related inner-product. By a
central plane signify any hyperplane including the origin and by
hemisphere either of the two separated sets of points of
S on one side of a central plane. By a
convex lune signify the intersection of (at most) two hemispheres.
We now specialize to the vector space
R3 with its usual inner-product, wherein central planes will have dimension two and meet any sphere (as defined!) in a circle, which we will call a
great circle. The same great circle may also be refered to as the boundary of a hemisphere on either side of the same central plane. By a
spherical triangle we will mean a non-empty intersection of
three hemispheres such that the great circles that are their boundaries intersect pairwise, but not all three together. We claim without proof that the notion of angle between vectors corresponding to the inner product on
R3 induces a notion of angle between hemispheres as well, and thus also an angle measure for lunes such that if a finite set of great circles and pairwise disjoint lunes has union the whole sphere, then the angles of those lunes have sum equal to 2π. Our final unproved claim is that both the property of being a lune and the angle of a lune are invariant under the action of the orthogonal group.
As a triangle
ABC is an intersection of three hemispheres
A,
B,
C, so the pairwise intersections of the same three hemispheres are three lunes
AB,
AC,
BC, and the angles of these three lunes shall be called also the angles of the triangle. Related to the three hemispheres are their oposite hemispheres also
A',
B',
C'; as these have the same respective boundaries, substituting any of
A',
B',
C' for
A,
B,
C, respectively, produces eight disjoint triangles (including ABC) --- we will extend the preceding notation for specific lunes and triangles to name these.
A more economical decomposition, however, is into the two disjoint triangles
ABC and
A'B'C', and the three lunes
AB', BC', A'C. (This is a tedious exercise in propositional logic, or an easy picture to draw). Remark that
AB and
A'B' have the same angle, as have
AB' and
A'B.
These four lunes are disjoint and, together with the boundaries of
A and
B, they have union the whole sphere, so the angles of
AB and
AB' are suplementary. Similarly are the angles
BC and
BC',
AC and
A'C. The three lunes
AB', BC', A'C, thus have angles summing to 3π less the sum of the angles of
ABC. There is no finite set of great circles whose union together with that of the three triangles is the whole sphere; if three lunes orthogonally equivalent to
AB', BC', A'C together with one more
did give the whole sphere, then the fourth lune must have angle equal to the sum of the angles of
ABC less π.
Sometimes a classical geometer