The canonical bidual map is an isometry

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 the norming-functional supplier [F2] in step 2.1.

From The canonical evaluation map into the bidual, with its stated hypotheses: Let $\mathbb{K}=\mathbb{R}$ or $\mathbb{C}$. For a normed $X$, define $J_X:X\to X^{\ast \ast },(J_{X}x)(f)=f(x)(f\in X^{\ast })\mathrm{.}$ With the dual norm from def-dual-space-of-a-normed-space, evaluation is linear in $f$ and $\mathrm{\mid }(J_{X}x)(f)\mathrm{\mid }\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }f\mathrm{\parallel }$, so $J_{X}x$ is a bounded functional on $X^{\ast }$. The map is canonical and uses no chosen basis or conjugation.

From Every nonzero vector has a norming functional, with its stated hypotheses: Let $X$ be a normed space over $\mathbb{R}$ or $\mathbb{C}$, and let $x\in X$ be nonzero. Then there exists $f\in X^{\ast }$ such that $\mathrm{\parallel }f\mathrm{\parallel }=1\text{and}f(x)=\mathrm{\parallel }x\mathrm{\parallel }\mathrm{.}$