Proof for spherical polar law of cosine I'm reading my textbook and for some reason, it does not present the proof for the spherical polar law of cosine which is:
$$ \cos(a)=\frac{\cos(A)+\cos(B)\cos(C)}{\sin(B) \sin(C)}$$
It does present the proof for spherical law of cosine which is:
$$ \cos(A)=\frac{\cos(a)-\cos(b)\cos(c)}{\sin(b) \sin(c)}$$
where $A$ is the angle and $a,b,c$ are the sides.
in which they use cross product and dot product where for example $|b\times c|=\sin a$ and $(b,c)=\cos a$. So i'm not sure but I believe that for the proof for the spherical polar law of cosine, it can use a similar method. However, like i said, i'm not sure. For example, does $|B\times C|=\sin A$ ?
If anyone can help start this proof or show me, either way that would be great. 
 A: If you write $\lvert b\times c\rvert=\sin a$, then $b$ and $c$ are vectors, while $a$ is an angle (or the length of the geodesic, which is the same thing). So you might want to use different symbols. There are actually four distinct sets of symbols you might want to use:


*

*The positions of the corners: $A,B,C\in S^2$

*The angles at these corners: $\alpha,\beta,\gamma\in\mathbb R$

*The geodesic lengths of the edges: $a,b,c\in\mathbb R$

*The polar vectors of the edges: $n_a,n_b,n_c\in S^2$


The polar vector of an edge is the vector pointing to a pole if you consider that edge as the equator. Or in other words, it's the unit normal vector perpendicular to the plane of the corresponding great circle. This vector can be used to express the angle between two geodesics: it's simply the same as the angle between the corresponding polar vectors (at least as long as you got the signs right, see below). So using this, you can formulate things like $\lvert n_b\times n_c\rvert=\sin \alpha$ as well as $\lvert B\times C\rvert=\sin a$.
In fact there is a very simple translation: if you exchange $A,B,C$ with $n_a,n_b,n_c$ and $\alpha,\beta,\gamma$ with $a,b,c$ you get the polar version of every trigonometric statement. You might want to take special care of orientation. Things would be reall ysimple in elliptic geometry, where you consider antipodal points as equivalent. In spherical geoemtry, antipodal points are distinct, and great circle arcs come with an orientation (depending on which of the two possible normal vectors you choose). Picking the wrong one will give you an incorrect sign for one of these vectors, and may later on result in a complimentary angle. But apart from such minor details, the translations should be straight forward.
A: Here is a different proof from Boris Springborn's lecture notes from the TU Berlin, which uses the Gram matrix to obtain the side cosine, angle cosine and four more equations by simultaneous permutations of $a,b,c$ and $\alpha^\prime, \beta^\prime,\gamma^\prime$.
Proof: 
Let $V = \left(A \ B \ C\right) \in \mathbb{R}^{3 \times 3}$ be the matrix whose columns are the vertices of the spherical triangle, cosidered as column vectors. Then the Gram matrix for $A,B,C$ is $$
G = V^TV= \begin{pmatrix} 
\langle A,A\rangle & \langle A,B\rangle & \langle A,C\rangle \\
\langle B,A\rangle & \langle B,B\rangle & \langle B,C\rangle \\
\langle C,A\rangle & \langle C,B\rangle & \langle C,C\rangle \\
\end{pmatrix} = \begin{pmatrix} 
1 & \cos c & \cos b \\
\cos c & 1 & \cos a \\
\cos b & \cos a & 1 \\
\end{pmatrix}.
$$
(Note for later that $\mathrm{det}(G) > 0$). Similarly, let $W = \left( A^\prime \ B^\prime \ C^\prime \right)$ be the matrix of poles. Their Gram matrix is $$
G^\prime = W^TW = \begin{pmatrix} 
\langle A^\prime,A^\prime\rangle & \langle A^\prime,B^\prime\rangle & \langle A^\prime,C^\prime\rangle \\
\langle B^\prime,A^\prime\rangle & \langle B^\prime,B^\prime\rangle & \langle B^\prime,C^\prime\rangle \\
\langle C^\prime,A^\prime\rangle & \langle C^\prime,B^\prime\rangle & \langle C^\prime,C^\prime\rangle \\
\end{pmatrix} = \begin{pmatrix} 
1 & \cos \gamma^\prime & \cos \beta^\prime \\
\cos \gamma^\prime& 1 & \cos \alpha^\prime \\
\cos \beta^\prime & \cos \alpha^\prime & 1 \\
\end{pmatrix}.
$$.
Also,
$$
W^TV= \begin{pmatrix} 
\langle A^\prime,A\rangle & \langle A^\prime,B\rangle & \langle A^\prime,C\rangle \\
\langle B^\prime,A\rangle & \langle B^\prime,B\rangle & \langle B^\prime,C\rangle \\
\langle C^\prime,A\rangle & \langle C^\prime,B\rangle & \langle C^\prime,C\rangle \\
\end{pmatrix} = \begin{pmatrix} 
\langle A^\prime,A\rangle & 0 & 0 \\
0 & \langle B^\prime,B\rangle & 0 \\
0 & 0 & \langle C^\prime,C\rangle \\
\end{pmatrix} =\colon D.
$$ is a diagonal matrix with positive entries. So $W^T = DV^{-1}$ and $W = (V^t)^{-1}D$, and $$
G^\prime = DV^{-1}(V^T)^{-1}D = D(V^TV)^{-1}D = DG^{-1}D. \quad (\star)
$$
The inverse of $G$ is $$
G^{-1} = \frac{1}{\det(G)}\begin{pmatrix} 
\sin^2 a & -\cos c + \cos a \cos b & - \cos b + \cos c \cos a \\
-\cos c + \cos a \cos b & \sin^2 b & -\cos a + \cos b \cos c \\
- \cos b + \cos c \cos a  & -\cos a + \cos b \cos c & \sin^2 c
\end{pmatrix}.
$$
Substitute this into $(\star)$ and consider diagonal elements: 
One finds $1 = D_{11}^{2} \frac{1}{\mathrm{det}(G)}\sin^2 a$, therefore $D_{11} = \frac{\sqrt{\mathrm{det}(G)}}{\sin a}$, andsimilarly $D_{22} =\frac{\sqrt{\mathrm{det}(G)}}{\sin b}$,$D_{33} = \frac{\sqrt{\mathrm{det}(G)}}{\sin c}$. Now consider for example element $(3,2)$ in $(\star)$:$$
\cos \alpha^\prime = D_{33}\frac{1}{\mathrm{det}(G)}\left(-\cos a + \cos b \cos c \right)D_{22}. \qquad \text{(Convince yourself!)}
$$
This is the side cosine theorem: $\cos \alpha^\prime = \frac{-\cos a + \cos b \cos c}{\sin b \sin c}$. The angle cosine theorem is the side cosine theorem applied to the polar triangle. Hence, $\cos a = \frac{-\cos \alpha^\prime + \cos \beta^\prime \cos \gamma^\prime}{\sin \beta^\prime \sin \gamma^\prime}$.
