Nice proof of the triangle inequality for the metric of the hyperbolic plane I am writing something for the journal of the university on the Lorentz space, and I want to prove that the following definition of the hyperbolic distance on the upper sheet of the hyperboloid $v \cdot v=-1$ is a metric:
The hyperbolic distance between $u$ and $v$ is the only positive number $\eta (u,v)$ such that
$$\cosh(\eta(u,v))=-u \cdot v.
$$
The first properties are easy, but all the proofs of the triangle inequality that I have seen seem complicated. In Ratcliffe's Foundations of Hyperbolic Manifolds the lorentzian cross product is used along with many of its properties, and I would like not having to introduce the cross product just for this proof.
I have thought about showing that the hyperbolic angle is the same as the lorentzian arc-length distance, and then showing that the metric given by the arc length satisfies the triangle inequality, but this seems even more tedious. Is there a shorter and nicer proof of this?
 A: The inequality we want to prove is
$$
\left|\frac{u-v}{1-\overline{u}v}\right| \le 
\left|\frac{u-a}{1-\overline{u}a}\right| + 
\left|\frac{a-v}{1-\overline{a}v}\right|
$$
for $u,v,a$ in the open unit disk ${\mathbf D}$. Let $f$ be the map
$$ 
f(\zeta)=\frac{\zeta-a}{1-\overline{a}\zeta} \quad (\zeta \in {\mathbf D}).
$$
It is easily seen that $f$ maps ${\mathbf D}$ into itself. Indeed, if $\zeta,a \in {\mathbf D}$, then $(1-|\zeta|^2)(1-|a|^2)> 0$, it follows that
$|\zeta|^2+|a|^2 < 1+ |a|^2 |\zeta|^2$, and after adding $-\overline{a}\zeta-a\overline{\zeta}$ on both sides, we get
$ 
|\zeta-a|^2 < |1-\overline{a}\zeta|^2$, that is 
$f(z)=\frac{\zeta-a}{1-\overline{a}\zeta} \in {\mathbf D}$.
A straightforward computation shows that 
$$
\left|\frac{f(\zeta)-f(\xi)}{1-\overline{f(\zeta)}f(\xi)}\right|
=\left|\frac{\zeta-\xi}{1-\overline{\zeta}\xi}\right|.
$$
Thus, in the inequality we want to prove we may replace $u,v,a$ by $f(u)=:z$,
$f(v)=:w$, $f(a)=0$, respectively, and we are left with proving that
$$
\left|\frac{z-w}{1-\overline{z}w}\right| \le |z|+|w|,
$$
that is,
$$ 
|z-w| \le |z|\,|1-\overline{z}w|+|w|\,|1-\overline{z}w|
$$
for $z,w \in {\mathbf D}$. Since $|1-\overline{z}w|=|1-\overline{w}z|$,
this is equivalent to the inequality
$$
|z-w| \le |z-|z|^2 w|+|w-|w|^2z|.
$$
Denote the points $z$ and $w$ in the complex plane by $Z$ and $W$, and let
$O$ denote the origin. The point $|z|^2w$ is a point $P$ on the line segment
between $O$ and $W$, and $z-|z|^2w$ is the vector from $P$ to $Z$.
It follows that $|z-|z|^2w|$ equals the (Euclidean) length $|PZ|$ of
the line segment between $P$ and $Z$. Analogously, $|w-|w|^2z|=|QW|$ for
some point $Q$ on the line segment between $O$ and $Z$. Let $S$ be the
point of intersection of the line segments $PZ$ and $QW$. We then have
$$
|z-w|  =  |ZW| \le |ZS|+|SW| \le |PZ|+|QW| = |z-|z|^2 w|+|w-|w|^2z|,
$$
which is what we wanted to prove. 
A: We need to check $\eta(u,v)+\eta(v,w)\ge\eta(u,w)$. Introduce coordinates $x,y,z$ so that the form is $x^2+y^2-z^2$.
First, verify that there is a Lorentz map sending $v$ to $(0,0,1)$. Since it is an isometry, we may now assume that $v=(0,0,1)$. This is the main idea. For added convenience, you may also rotate the $xy$-plane so that the $y$-coordinate of $u$ equals 0.
Next, observe that the formula yields equality in the case when the projections of $u$ and $w$ to the $xy$-plane are endpoints of a segment containing (0,0). This is straigtforward if you write $u=(\sinh a,0,\cosh a)$ and $w=(-\sinh b,0,\cosh b)$ where $a,b\ge 0$.
Finally, rotate $w$ around the $z$-axis until it comes to a position as above. The product $u\cdot w$ grows down (it equals contant plus the scalar product of the $xy$-parts, since $z$-coordinates are fixed). Hence $\eta(u,w)$ grows up while the two other distances stay, q.e.d.
Of course, for writing purposes the last step is just an application of Cauchy-Schwarz for the scalar product in $\mathbb R^2$.
This was about two-dimensional hyperbolic plane, in higher dimensions just insert more coordinates (they will not actually show up in formulae).
