Proving pseudo-hyperbolic distance is distance The pseudo-hyperbolic distance on the unit disk is defined as:
$$\rho(z,w)=\left|\dfrac{z-w}{1-\bar wz}\right|.$$
I'd like to prove it's a distance. The real problem is, as always, the triangle inequality, because the other properties are mostly obvious. That is, I need to prove:
$$\rho(z,w)\leq\rho(z,t)+\rho(t,w),$$
for all $z,w,t\in\mathbb{D}$. I tried writing $z,t,w$ as real part plus $i$ times imaginary part, and ended up with a messy expression Wolfram can't handle. I tried polar coordinates, and the mess is even worse, and Wolfram's help is even less. I Googled first, but only found stuff about the Hyperbolic distance, and a pdf having this as an exercise, suggesting to also show that:
$$\rho(z,w)\leq\frac{\rho(z,t)+\rho(t,w)}{1+\rho(z,t)\rho(t,w)}.$$
But that didn't help. So here I am. How do I solve this?
 A: It helps to know that $\rho$ is invariant under Möbius transformations. Indeed, $\rho(z,w)=|\phi(z)|$ where $\phi$ is any Möbius map such that $\phi(w)=0$ (they all agree up to rotation, which doesn't change the modulus). Since Möbius maps form a group, applying one of them to both $z$ and $w$ does not affect the above formula for $\rho$. 
In order to prove the triangle inequality, first map $t$ to $0$ by a suitable Möbius map. This reduces the task to
$$\left|\frac{z-w}{1-z\overline w}\right|\le |z|+|w| \tag{1}$$
Let $|z|=a$, $|w|=b$, and let $\theta $ be the polar angle between $z$ and $w$. Then $(1)$ becomes
$$ \frac{a^2+b^2-2ab\cos\theta }{1+a^2b^2-2ab\cos\theta } \le (a+b)^2 \tag{2}$$
To estimate the left side, rewrite it as 
$$
1 - \frac{(1-a^2)(1-b^2) }{1+a^2b^2-2ab\cos\theta }
\le 
1 - \frac{(1-a^2)(1-b^2) }{1+a^2b^2+2ab } =\frac{(a+b)^2}{(1+ab)^2} $$ and $(2)$ follows.
A: $\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\lbar}{\overline}$
Expanding on Homegrown Tomato's answer.
Introducing disk automorphism as a means to simplify the thesis
It can be proven that holomorphic functions decrease the pseudo-hyperbolic distance, i.e. if $f$ is holomorphic then $\rho(f(z),f(w))\leq\rho(z,w)$ for all $z,w\in\mathbb{D}$. It is then easy to prove that the automorphism of the unit disk fix that distance, since both they and their inverses decrease it.
Let us prove the above claim. Let us write it explicitly:
$$\abs{\frac{f(z)-f(w)}{1-\lbar{f(w)}f(z)}}\leq\abs{\frac{z-w}{1-\lbar wz}}.$$
If we set:
$$\psi_w(z)=\frac{z-w}{1-\lbar wz}$$
for any $z,w\in\mathbb{D}$, then the thesis becomes:
$$\abs{\psi_{f(w)}(f(z)\!)}\leq\abs{\psi_w(z)}.$$
The function $\psi_{f(w)}\circ f\circ\psi_w$ is holomorphic, sends the disk into itself, and fixes 0. Thus, by Schwarz's lemma, we know that if $z,w\in\mathbb{D}$:
$$\abs{\psi_{f(w)}\circ f\circ\psi_w(z)}\leq\abs{z}.$$
That this function fixes 0 is because $\psi_w$ sends 0 to $w$, then $f$ sends it to $f(w)$ and $\psi_{f(w)}(f(w))=0$. Now set $z'=\psi_w(z)$, and remembering $\psi_w$ is its own inverse we know that $z=\psi_w(z')$, so the inequality above becomes:
$$\abs{\psi_{f(w)}(f(z'))}\leq\abs{\psi_w(z')},$$
which is the claim, save for $z$ having turned to $z'$.
Reducing the inequality to something simpler
That being said, we return to the topic of this question. Let $z,w,t\in\mathbb{D}$. We need to prove that:
$$\rho(z,w)\leq\rho(z,t)+\rho(t,w).$$
Let us write the distances explicitly:
$$\abs{\frac{z-w}{1-\lbar wz}}\leq\abs{\frac{z-t}{1-\lbar tz}}+\abs{\frac{t-w}{1-\lbar wt}}.$$
Since $\psi_t$ fixes the pseudo-hyperbolic distance, we can apply it to $z,w,t$ and if the inequality is proven after applying $\psi_t$, it holds before too. Applying $\psi_t$ maps $t$ to 0, and setting $z'=\psi_t(z),w'=\psi_t(w)$, the inequality becomes:
$$\abs{\frac{z'-w'}{1-\lbar{w'}z'}}\leq\abs{\frac{z'-0}{1-\lbar0z'}}+\abs{\frac{0-w'}{1-\lbar{w'}0}}=\abs{z'}+\abs{w'}.$$
Very long computations to prove the simpler thing
We focus on this last inequality and forget about the primes. We set $z=re^{i\theta},w=\rho e^{i\phi}$. The inequality then becomes… well, let us first square the inequality and then calculate the members bit by bit:
$$\abs{\frac{z-w}{1-\lbar wz}}^2\leq(\abs{z}+\abs{w})^2=\abs{z}^2+\abs{w}^2+2\abs{zw}.$$
The numerator on the left is:
\begin{align*}
\abs{z-w}^2={}&\abs{r\cos\theta-\rho\cos\phi+i(r\sin\theta-\rho\sin\phi)}^2={} \\
{}={}&(r\cos\theta-\rho\cos\phi)^2+(r\sin\theta-\rho\sin\phi)^2={} \\
{}={}&r^2\cos^2\theta+\rho^2\cos^2\phi-2r\rho\cos\theta\cos\phi+r^2\sin^2\theta+\rho^2\sin^2\phi-2r\rho\sin\theta\sin\phi={} \\
{}={}&r^2+\rho^2-2r\rho(\cos\theta\cos\phi+\sin\theta\sin\phi)={} \\
{}={}&r^2+\rho^2-2r\rho\cos\theta',
\end{align*}
where we have set $\theta'=\theta-\phi$. The denominator on the left is:
\begin{align*}
\abs{1-\lbar wz}^2={}&\abs{1-r\rho e^{i\theta'}}^2=\abs{1-r\rho\cos\theta'-ir\rho\sin\theta'}^2=(1-r\rho\cos\theta')^2+r^2\rho^2\sin^2\theta'={} \\
{}={}&1+r^2\rho^2\cos^2\theta'-2r\rho\cos\theta'+r^2\rho^2\sin^2\theta'=1+r^2\rho^2-2r\rho\cos\theta'.
\end{align*}
And the right side is simply $(r+\rho)^2$. So the inequality has become:
$$\frac{r^2+\rho^2-2r\rho\cos\theta'}{1+r^2\rho^2-2r\rho\cos\theta'}\leq(r+\rho)^2.$$
I used different names, precisely I called $r$ what Homegrown Tomato called $a$, $\rho$ what he called $b$, and $\theta'$ what he called $\theta$, but this is precisely his (2). We now add and subtract $1+r^2\rho^2$ to the numerator, getting $r^2+\rho^2-2r\rho\cos\theta'+r^2\rho^2+1-1-r^2\rho^2$, but the terms in the middle simplify and give us a nice 1, whereas the rest leaves us with $r^2+\rho^2-1-r^2\rho^2=-(1-r^2)(1-\rho^2)$. So the inequality is rewritten as:
$$1-\frac{(1-r^2)(1-\rho^2)}{1+r^2\rho^2-2r\rho\cos\theta'}.$$
Now we notice that $\cos\theta'\geq-1$. Since $a,b\geq0$, this means $-2ab\cos\theta'\leq2ab$. Thus, $1+a^2b^2-2ab\cos\theta\leq1+a^2b^2+2ab=(1+ab)^2$. Put it in the denominator, and the inequality flips. Put a minus before the fraction, and the inequality gets back to $\leq$. And we are in our situation, which means that:
$$1-\frac{(1-a^2)(1-b^2)}{1+a^2b^2-2ab\cos\theta}\leq1-\frac{(1-a^2)(1-b^2)}{(1+ab)^2}.$$
Oh sorry, I switched to Homegrown Tomato's names :). In my names, that would be:
$$1-\frac{(1-r^2)(1-\rho^2)}{1+r^2\rho^2-2r\rho\cos\theta'}\leq1-\frac{(1-r^2)(1-\rho^2)}{(1+r\rho)^2}.$$
Now we make that sum, and we get the same denominator, and $1+r^2\rho^2+2r\rho-1+r^2+\rho^2-r^2\rho^2=r^2+\rho^2+2r\rho=(r+\rho)^2$, so finally our inequality reads:
$$\abs{\frac{z-w}{1-\lbar wz}}^2=\frac{r^2+\rho^2-2r\rho\cos\theta'}{1+r^2\rho^2-2r\rho\cos\theta'}\underset{\substack{|\\\text{Just proven}}}{\leq}\frac{(r+\rho)^2}{(1+r\rho)^2}\underset{\substack{|\\\text{To be proven yet}}}{\leq}(r+\rho)^2=(\abs{z}+\abs{w})^2.$$
It then suffices to show that $(1+r\rho)^2\geq1$, which is pretty evident since $1+r\rho$ is one plus something non-negative, thus $1+r\rho\geq1$, and so is its square.
