Distance to a subspace via annihilating functionals

For $f\in M^{\perp }$ with $\mathrm{\parallel }f\mathrm{\parallel }\le 1$, continuity gives $f{\mathrm{\mid }}_{\bar{M}}=0$. Hence, for every $m\in \bar{M}$, $\mathrm{\mid }f(x)\mathrm{\mid }=\mathrm{\mid }f(x-m)\mathrm{\mid }\le \mathrm{\parallel }x-m\mathrm{\parallel }$. Taking infima gives the $\le$ direction.

Put $\delta =\mathrm{dist}(x,\bar{M})$. If $\delta >0$, define $g:\bar{M}+\mathbb{K}x\to \mathbb{K}$ by $g(m+\lambda x)=\lambda \delta$. This is well defined, and $\mathrm{\mid }g(m+\lambda x)\mathrm{\mid }=\mathrm{\mid }\lambda \mathrm{\mid }\delta \le \mathrm{\parallel }m+\lambda x\mathrm{\parallel },$ so $\mathrm{\parallel }g\mathrm{\parallel }\le 1$. In the real case apply [F1] with $p(y)=\mathrm{\parallel }y\mathrm{\parallel }$; domination at $y$ and $-y$ gives an extension $f$ with $\mathrm{\parallel }f\mathrm{\parallel }\le 1$. In the complex case apply [F1] to $\mathrm{Re}g$ on the underlying real subspace, obtaining a real linear $U$ with $\mathrm{\mid }U(y)\mathrm{\mid }\le \mathrm{\parallel }y\mathrm{\parallel }$. Then $f(y)=U(y)-iU(iy)$ is complex linear and extends $g$. For each $y$, choose a scalar $a$ of modulus one with $af(y)=\mathrm{\mid }f(y)\mathrm{\mid }$; thus $\mathrm{\mid }f(y)\mathrm{\mid }=U(ay)\le \mathrm{\parallel }y\mathrm{\parallel }$. This is the exact use of AC in both scalar cases; this extension lies in $M^{\perp }$ and satisfies $\mathrm{\mid }f(x)\mathrm{\mid }=\delta$. If $\delta =0$, then $x\in \bar{M}$, so continuity makes every annihilator vanish at $x$. Thus equality holds in both cases.