Eberlein–Šmulian metrization on the relevant dual ball

If $Y=\{0\}$, then $K$ is either empty or the singleton $\{0\}$. In either case the zero function $d_K:K\times K\to \mathbb{R}$ is the unique metric and induces the only topology on $K$, which is its relative weak topology. Hence suppose below that $Y\mathrm{\ne }\{0\}$.

On $\mathbb{K}$ put $\delta (s,t)=\min \{1,\mathrm{\mid }s-t\mathrm{\mid }\}$. This is a metric bounded by $1$ and induces the usual scalar topology, because its balls of radius below $1$ are the usual metric balls. It is complete: a $\delta$-Cauchy sequence is eventually Cauchy for $\mathrm{\mid }\cdot \mathrm{\mid }$ at every tolerance below $1$, so [F5] gives a usual limit, and $\delta (s,t)\le \mathrm{\mid }s-t\mathrm{\mid }$ gives convergence in $\delta$.

By separability, take an at most countable norm-dense $D\subseteq Y$. It is nonempty because its closure is the nonempty space $Y$. The set $E=\{z\mathrm{/}\mathrm{\parallel }z\mathrm{\parallel }:z\in D\setminus \{0\}\}$ is at most countable and nonempty. It is dense in the unit sphere: if $\mathrm{\parallel }u\mathrm{\parallel }=1$ and $\epsilon >0$, density gives $z\in D$ with $\mathrm{\parallel }z-u\mathrm{\parallel }<\min \{1\mathrm{/}2,\epsilon \mathrm{/}2\}$, so $z\mathrm{\ne }0$ and $\mathrm{\parallel }z\mathrm{/}\mathrm{\parallel }z\mathrm{\parallel }-u\mathrm{\parallel }\le \mathrm{\mid }1-\mathrm{\parallel }z\mathrm{\parallel }\mathrm{\mid }+\mathrm{\parallel }z-u\mathrm{\parallel }\le 2\mathrm{\parallel }z-u\mathrm{\parallel }<\epsilon$. By [F1], enumerate $E$ as $(u_n{)}_{n\in \mathbb{N}}$, allowing repetitions.

Apply [F6] to countably many copies of $(\mathbb{K},\delta )$. The formula $D(a,b)={\sum }_{n=0}^{\mathrm{\infty }}{2}^{-(n+1)}\delta (a_n,b_n)$ is a metric on ${\mathbb{K}}^{\mathbb{N}}$ inducing its product topology. Its restriction to every subset is a metric inducing the subspace topology, and that metric topology is Hausdorff by [F7].

For each $n$, let $S_n=\{f\in Y^{\ast }:\mathrm{\parallel }f\mathrm{\parallel }=1,f(u_n)=1\}$. Each $S_n$ is nonempty by [F2], including in the complex case where the attained value is the positive real number $1$. Apply ${\mathrm{A}\mathrm{C}}_{\omega }$ once to the sequence $(S_n)$ and obtain $f_n\in S_n$ for every $n$.

The family $(f_n)$ separates points of $Y$. If $x\mathrm{\ne }y$, put $v=(x-y)\mathrm{/}\mathrm{\parallel }x-y\mathrm{\parallel }$ and choose $u_n$ with $\mathrm{\parallel }{u}_n-v\mathrm{\parallel }<1\mathrm{/}2$. Then $\mathrm{\mid }{f}_n(v)\mathrm{\mid }\ge \mathrm{\mid }{f}_n(u_n)\mathrm{\mid }-\mathrm{\mid }{f}_n(v-u_n)\mathrm{\mid }>1-1\mathrm{/}2>0$, since $\mathrm{\parallel }{f}_n\mathrm{\parallel }=1$. Therefore $f_n(x-y)=\mathrm{\parallel }x-y\mathrm{\parallel }{f}_n(v)\mathrm{\ne }0$.

Define $\mathrm{\Phi }:K\to {\mathbb{K}}^{\mathbb{N}}$ by $\mathrm{\Phi }(x)=(f_n(x){)}_n$. Every coordinate $f_n$ is weakly continuous, so the initial property of the product topology makes $\mathrm{\Phi }$ continuous. Step 4.1 makes it injective. Its corestriction ${\mathrm{\Phi }}_0:K\to \mathrm{\Phi }[K]$ is therefore a continuous bijection.

The weak space $K$ is compact by hypothesis, and $\mathrm{\Phi }[K]$ is Hausdorff by step 2.2. Hence [F8] makes ${\mathrm{\Phi }}_0$ a homeomorphism. Pulling the restricted product metric back along ${\mathrm{\Phi }}_0$ gives exactly $d_K(x,y)=D(\mathrm{\Phi }(x),\mathrm{\Phi }(y))$, the displayed metric, and its topology is precisely the relative weak topology on $K$. Together with step 1.1 this proves the claim for every $Y$ and for empty as well as nonempty $K$.

The only countable selection is step 3.1, where ${\mathrm{A}\mathrm{C}}_{\omega }$ selects the norming family. HB is used only inside the individual norming-functional supplier [F2]. Enumeration in step 2.1 is obtained from one at-most-countable set by its supplied surjection and uses no choice. The argument metrizes only the supplied weakly compact $K$ in a separable $Y$; it makes no metrizability claim for all of $Y$ or for nonseparable spaces.