Distance to a closed subspace via unit annihilators

Given: The Axiom of Choice, The spaces, maps, scalar field, and hypotheses in the statement above. All duals consist of linear functionals over the ambient field; evaluation has no conjugation.

AC is used through bidual norm equality [F2] in step 1.1.

From The dual of a quotient is its annihilator, with its stated hypotheses: Let $\mathbb{K}=\mathbb{R}$ or $\mathbb{C}$. Let $X$ be normed and $M\le X$ closed. With quotient norm $\mathrm{\parallel }x+M\mathrm{\parallel }={\inf }_{m\in M}\mathrm{\parallel }x+m\mathrm{\parallel }$ and $q(x)=x+M$, the map $Q:(X\mathrm{/}M{)}^{\ast }⟶M^{\perp },Qh=h\circ q$ is a linear isometric bijection.

From The canonical bidual map is an isometry, with its stated hypotheses: Let $\mathbb{K}=\mathbb{R}$ or $\mathbb{C}$. For every normed $X$, the map $J_X:X\to X^{\ast \ast }$ is linear and $\mathrm{\parallel }{J}_{X}x\mathrm{\parallel }=\mathrm{\parallel }x\mathrm{\parallel }$ for every $x\in X$. In particular it is injective.