The dual of a closed subspace is a dual quotient

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 norm-preserving extension [F4] in steps 2.1 and 3.1.

From Annihilator notation and the preannihilator, with its stated hypotheses: Let $\mathbb{K}=\mathbb{R}$ or $\mathbb{C}$. For a normed $X$ and arbitrary subsets $M\subseteq X$, $N\subseteq X^{\ast }$, define $M^{\perp }=\{f\in X^{\ast }:f(m)=0\text{ for all }m\in M\},{}^{\perp }N=\{x\in X:f(x)=0\text{ for all }f\in N\}\mathrm{.}$ Here $X^{\ast }$ is def-dual-space-of-a-normed-space. The first notation agrees with def-continuous-annihilator-of-a-subspace on $\mathrm{span}M$, since linearity makes vanishing on $M$ equivalent to vanishing on its span. The preannihilator lies in $X$, not in $X^{\ast \ast }$. Empty sets impose no conditions: ${\mathrm{\varnothing }}^{\perp }=X^{\ast }$ and ${}^{\perp }\mathrm{\varnothing }=X$.

From Annihilators and preannihilators are norm closed, with its stated hypotheses: Let $\mathbb{K}=\mathbb{R}$ or $\mathbb{C}$. For any normed $X$ and arbitrary $M\subseteq X$, $N\subseteq X^{\ast }$, both $M^{\perp }\subseteq X^{\ast }$ and ${}^{\perp }N\subseteq X$ are norm-closed linear subspaces. Moreover ${\bar{N}}^{\mathrm{\parallel }\cdot \mathrm{\parallel }}\subseteq ({}^{\perp }N{)}^{\perp }$.

From A bounded operator that vanishes on a subspace factors uniquely through the normed quotient, with its stated hypotheses: Let $X$ and $Y$ be normed spaces over the same scalar field, let $M\le X$ be a closed linear subspace, let $q:X\to X\mathrm{/}M$ be the quotient map, and let $T:X\to Y$ be a bounded linear operator with $M\subseteq \ker T$. Then there is a unique bounded linear operator $\bar{T}:X\mathrm{/}M\to Y$ such that $\bar{T}\circ q=T,$ and moreover $\mathrm{\parallel }\bar{T}\mathrm{\parallel }=\mathrm{\parallel }T\mathrm{\parallel }$.

From A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed, with its stated hypotheses: Let $X$ be a normed space over $\mathbb{R}$ or $\mathbb{C}$, let $M\subseteq X$ be a linear subspace, and let $f_0:M\to \mathbb{R}$ or $f_0:M\to \mathbb{C}$ be a bounded linear functional over the ambient scalar field. Then there exists a bounded linear extension $F$ of $f_0$ to all of $X$ such that $\mathrm{\parallel }F\mathrm{\parallel }=\mathrm{\parallel }{f}_0\mathrm{\parallel }$. No closedness hypothesis on $M$ is needed.