C$^*$-algebras: When is there equality in the triangle inequality? (I had never thought about this question before, and I want to record the basic answer here for future reference)
Let $A$ be a C$^*$-algebra, and $x,y\in A$. When do we have equality in the triangle inequality? $$\|x+y\|=\|x\|+\|y\|$$
 A: Given $x,y\in A$, it turns out that the following statements are equivalent:


*

*(i) $\|x+y\|=\|x\|+\|y\|$



*

*(ii) there exists a norm-one linear functional $f$ such that $f(x)=\|x\|$, $f(y)=\|y\|$



*

*(iii) there exists a state  $g$ such that $g(x^*y)=\|x\|\,\|y\|$

Proof.
(i)$\implies$(ii) Let $f$ be a norm-one linear functional such that $f(x+y)=\|x+y\|$. Then
$$
f(x)+f(y)=f(x+y)=\|x+y\|=\|x\|+\|y\|.$$As we also have $|f(x)|\leq\|x\|$ and $|f(y)|\leq\|y\|$, it follows that $|f(x)|=\|x\|$, $|f(y)|=\|y\|$. As $$f(x)+f(y)=f(x+y)=\|x+y\|=\|x\|+\|y\|=|f(x)|+|f(y)|,$$ we deduce that  $f(x)=|f(x)|=\|x\|$, $f(y)=|f(y)|=\|y\|$.
(ii)$\implies$(iii) See below for the existence of the absolute value $g$ of the  functional $f$, which is a state since $\|f\|=1$. We have
\begin{align}
\|x\|^2+\|y\|^2+2\|x\|\,\|y\|&=(\|x\|+\|y\|)^2=f(x+y)^2=|f(x+y)|^2\\ \ \\
&=|g(v(x+y))|^2\\ \ \\
&\leq g((x+y)^*v^*v(x+y))\leq g((x+y)^*(x+y))\\ \ \\
&=g(x^*x)+g(y^*y)+2\operatorname{Re}g(x^*y)\\ \ \\
&\leq \|x\|^2+\|y\|^2+2|g(x^*y)|.
\end{align}
We then have
$$
\|x\|\,\|y\|\leq|g(x^*y)|\leq \|x\|\,\|y\|,
$$
impliying equality. From the inequalities above we also get $|g(x^*y)|=\operatorname{Re}g(x^*y)$, so $|g(x^*y)|=g(x^*y)$.
(iii)$\implies$(i)  We have, using Cauchy-Schwarz,
\begin{align}
\|x\|^2\|y\|^2=|g(x^*y)|^2\leq g(x^*x)g(y^*y)\leq\|x\|^2\,\|y\|^2.
\end{align}
Thus $g(x^*x)=\|x\|^2$, $g(y^*y)=\|y\|^2$.
Then
\begin{align}
(\|x\|+\|y\|)^2
&=\|x\|^2+\|y\|^2+2\|x\|\,\|y\|
=g(x^*x)+g(y^*y)+2g(y^*x)\\ \ \\
&=g((x+y)^*(x+y))\leq \|(x+y)^*(x+y)\|
=\|x+y\|^2. 
\end{align}
So $\|x\|+\|y\|\leq\|x+y\|$, and the reverse inequality is the triangle inequality.

Absolute value of a functional
Given a bounded linear functional $f$ on $A$, we may see $f$ as a normal functional in the double dual $A''$ and perform the polar decomposition of $f$. In other words, there exists a positive functional $g$ on $A$ (a state, since $\|f\|=1$) such that $f=g(v\cdot)$ for a partial isometry $v\in A''$.
