Goldstine's theorem

By [F1], $J_X(B_X)\subseteq B_{X^{\ast \ast }}$. This is where HB supplies the norm equality needed for the stated canonical isometric embedding.

Fix $x^{\ast \ast }\in B_{X^{\ast \ast }}$ and a basic weak-star neighborhood determined by $f_1,\dots ,f_m\in X^{\ast }$ and $\epsilon >0$. If $m=0$, it contains $J_X(0)$. Suppose $m\ge 1$, put $T(x)=(f_1(x),\dots ,f_m(x))$, $v=(x^{\ast \ast }(f_1),\dots ,x^{\ast \ast }(f_m))$, and let $C$ be the Euclidean closure of $T(B_X)$ in ${\mathbb{K}}^m$, viewed as ${\mathbb{R}}^m$ or ${\mathbb{R}}^{2m}$. The set $C$ is nonempty, closed and convex because $B_X$ is nonempty and convex and $T$ is real-linear.

If $v\mathrm{\notin }C$, [F2] gives a nonzero real-linear functional $\mathrm{\ell }$ and a real $b$ with $\mathrm{\ell }(z)\le b<\mathrm{\ell }(v)$ for every $z\in C$. Every real-linear functional on ${\mathbb{K}}^m$ has the form $\mathrm{\ell }(z)=\mathrm{Re}{\sum }_{j=1}^m{c}_j{z}_j$: in the complex case write its coefficients on real and imaginary coordinate vectors and take $c_j=a_j-i{b}_j$.

Put $f={\sum }_j{c}_j{f}_j\in X^{\ast }$. The separation inequalities give ${\sup }_{x\in B_X}\mathrm{Re}f(x)<\mathrm{Re}{x}^{\ast \ast }(f)$. Yet ${\sup }_{x\in B_X}\mathrm{Re}f(x)=\parallel f\parallel$: the inequality $\le$ is the norm bound, while for any $x$ rotate or change its sign so that $f(x)$ becomes the nonnegative real $\mathrm{\mid }f(x)\mathrm{\mid }$, and then take the supremum. Since $\parallel x^{\ast \ast }\parallel \le 1$, one also has $\mathrm{Re}{x}^{\ast \ast }(f)\le \mathrm{\mid }{x}^{\ast \ast }(f)\mathrm{\mid }\le \parallel f\parallel$.

The strict inequality in step 3.1 would therefore read $\parallel f\parallel <\mathrm{Re}{x}^{\ast \ast }(f)\le \parallel f\parallel$, which is impossible. Hence $v\in C$.

Because $v$ lies in the closure of $T(B_X)$, the open coordinate box $\{z:\mathrm{\mid }{z}_j-v_j\mathrm{\mid }<\epsilon ,1\le j\le m\}$ meets $T(B_X)$. Thus some $x\in B_X$ satisfies $\mathrm{\mid }{J}_X(x)(f_j)-x^{\ast \ast }(f_j)\mathrm{\mid }<\epsilon$ for every $j$, so $J_X(x)$ belongs to the chosen neighborhood.

Every basic weak-star neighborhood of every $x^{\ast \ast }\in B_{X^{\ast \ast }}$ therefore meets $J_X(B_X)$, including the empty-test and zero-space cases handled in step 1.2. This is exactly weak-star density.