[proofplan]
We pick a countable dense sequence $(x_n)$ in $X$ and, using [Hahn-Banach (Normed Space Version)](/theorems/2629), attach a unit-norm support functional $f_n$ at each $x_n$ with $f_n(x_n) = \|x_n\|_X$. The map $T: X \to \ell_\infty$ defined by $T(x) := (f_n(x))_{n \ge 1}$ is well-defined and contractive because $|f_n(x)| \le \|x\|_X$ for every $n$. The reverse bound $\|T(x)\|_{\ell_\infty} \ge \|x\|_X$ holds at each dense point $x_n$ by construction; we extend it to all of $X$ by continuity using the density of $(x_n)$.
[/proofplan]
[step:Choose a dense sequence and attach support functionals]
Since $X$ is separable, there exists a countable dense sequence $(x_n)_{n \ge 1}$ in $X$. We may assume $x_n \ne 0$ for every $n$, because the zero vector contributes nothing to density (removing it from a dense sequence preserves density when $X \ne \{0\}$; the case $X = \{0\}$ is handled by the zero embedding into $\ell_\infty$). For each $n$, the [Hahn-Banach (Normed Space Version)](/theorems/2629), part (ii) — the existence of a support functional — applied to the non-zero vector $x_n \in X$ produces $f_n \in X^*$ with
\begin{align*}
\|f_n\|_{X^*} = 1, \qquad f_n(x_n) = \|x_n\|_X.
\end{align*}
[guided]
The [Hahn-Banach (Normed Space Version)](/theorems/2629) part (ii) is the support-functional consequence of the extension theorem: for every $x \ne 0$ in a normed space, there exists a unit-norm functional $f$ with $f(x) = \|x\|$. Constructively, this $f$ is built by defining $g(\lambda x) := \lambda \|x\|$ on the one-dimensional subspace $\operatorname{span}\{x\}$ — then $g$ is linear with $|g(\lambda x)| = |\lambda|\|x\| = \|\lambda x\|$, so $\|g\| = 1$ on this subspace — and applying the norm-preserving extension version (part (i)) to extend $g$ to all of $X$.
The hypothesis $X^* \ne \emptyset$ in a non-trivial normed space is consumed exactly here: without Hahn-Banach we would have no guarantee that any non-zero continuous linear functional exists, let alone one of unit norm achieving $\|x_n\|_X$.
We need a separate $f_n$ for each $x_n$ because each $f_n$ is "tuned" to the corresponding $x_n$: it computes the exact value $\|x_n\|_X$ from $x_n$. The collection $(f_n)$ is the mechanism by which the embedding into $\ell_\infty$ recovers the norm of any $x \in X$ from the sequence $(f_n(x))$.
[/guided]
[/step]
[step:Define $T$ and verify $T(x) \in \ell_\infty$ with $\|T(x)\|_{\ell_\infty} \le \|x\|_X$]
Define
\begin{align*}
T: X &\to \ell_\infty \\
x &\mapsto (f_n(x))_{n \ge 1}.
\end{align*}
For every $n$ and every $x \in X$, the operator-norm bound for $f_n$ gives
\begin{align*}
|f_n(x)| \le \|f_n\|_{X^*} \|x\|_X = \|x\|_X.
\end{align*}
Hence $\sup_{n \ge 1} |f_n(x)| \le \|x\|_X < \infty$, so $T(x) \in \ell_\infty$ with
\begin{align*}
\|T(x)\|_{\ell_\infty} = \sup_{n \ge 1} |f_n(x)| \le \|x\|_X.
\end{align*}
Linearity of $T$ follows componentwise from the linearity of each $f_n$: for $x, y \in X$ and scalars $\lambda, \mu$,
\begin{align*}
T(\lambda x + \mu y) = (f_n(\lambda x + \mu y))_n = (\lambda f_n(x) + \mu f_n(y))_n = \lambda T(x) + \mu T(y).
\end{align*}
[/step]
[step:Verify equality $\|T(x_n)\|_{\ell_\infty} = \|x_n\|_X$ on the dense sequence]
For each fixed $n$, the upper bound from the previous step gives $\|T(x_n)\|_{\ell_\infty} \le \|x_n\|_X$. For the reverse direction, evaluating the supremum defining $\|T(x_n)\|_{\ell_\infty}$ at the index $n$ itself:
\begin{align*}
\|T(x_n)\|_{\ell_\infty} = \sup_{k \ge 1} |f_k(x_n)| \ge |f_n(x_n)| = \|x_n\|_X,
\end{align*}
where the final equality is the support-functional identity $f_n(x_n) = \|x_n\|_X$ from the first step. Combining the two bounds, $\|T(x_n)\|_{\ell_\infty} = \|x_n\|_X$.
[guided]
The identity $\|T(x_n)\|_{\ell_\infty} = \|x_n\|_X$ is the only place where the construction of $f_n$ as a support functional matters: at index $n$, the value $f_n(x_n)$ exactly recovers the norm. At all other indices $k \ne n$, we only know the upper bound $|f_k(x_n)| \le \|x_n\|_X$, which need not be tight. But to bound the supremum from below, a single witness — the diagonal index $k = n$ — suffices, and this witness is exactly $\|x_n\|_X$.
This is the geometric content of the proof: each dense vector $x_n$ has its own coordinate axis in $\ell_\infty$ on which it appears at full size.
[/guided]
[/step]
[step:Extend the isometry from the dense sequence to all of $X$ by continuity]
Both $\|\cdot\|_X: X \to \mathbb{R}$ and $\|T(\cdot)\|_{\ell_\infty}: X \to \mathbb{R}$ are continuous functions on $X$. The first is continuous because the norm on any normed space is $1$-Lipschitz (reverse triangle inequality). The second is continuous as the composition of $T: X \to \ell_\infty$ with the norm $\|\cdot\|_{\ell_\infty}$: $T$ is bounded (from step 2, $\|T(x)\|_{\ell_\infty} \le \|x\|_X$, so $T \in \mathcal{L}(X, \ell_\infty)$ with $\|T\| \le 1$) and the norm on $\ell_\infty$ is $1$-Lipschitz.
The set $\{x \in X : \|T(x)\|_{\ell_\infty} = \|x\|_X\}$ is therefore closed in $X$ as the preimage of the closed set $\{0\} \subset \mathbb{R}$ under the continuous function $x \mapsto \|x\|_X - \|T(x)\|_{\ell_\infty}$. The previous step shows this closed set contains every $x_n$, hence contains the closure $\overline{\{x_n : n \ge 1\}} = X$ (by density). So
\begin{align*}
\|T(x)\|_{\ell_\infty} = \|x\|_X \qquad \text{for all } x \in X.
\end{align*}
[guided]
We have an equality $\|T(x)\|_{\ell_\infty} = \|x\|_X$ on the dense set $\{x_n\}$ and want to upgrade it to all of $X$. This is the standard "continuity extends equalities from dense sets" pattern, and it has two ingredients:
1. **Continuity of both sides** as functions of $x$. The norm $\|\cdot\|_X$ is continuous (it is the norm itself). The map $x \mapsto \|T(x)\|_{\ell_\infty}$ is continuous because it is the composition of the bounded linear $T$ (which is continuous since bounded $\Leftrightarrow$ continuous for linear maps) with the continuous norm on $\ell_\infty$.
2. **Closedness of the equality set**: the set where two continuous real-valued functions agree is closed (preimage of $\{0\}$ under their difference).
Combining: the equality set is closed and contains the dense set $\{x_n\}$, so it contains the whole space.
What if $T$ were not bounded? Then $\|T(\cdot)\|_{\ell_\infty}$ might not be continuous, and the extension would fail. The bound $\|T(x)\|_{\ell_\infty} \le \|x\|_X$ from step 2 is therefore a load-bearing prerequisite for this continuity argument.
[/guided]
[/step]
[step:Conclude that $T$ is an isometric embedding]
The previous step shows $\|T(x)\|_{\ell_\infty} = \|x\|_X$ for every $x \in X$, so $T: X \to \ell_\infty$ preserves norms. This forces injectivity: if $T(x) = T(y)$ then $T(x - y) = 0$ by linearity, and $\|x - y\|_X = \|T(x - y)\|_{\ell_\infty} = 0$, so $x = y$.
The image $T(X) \subseteq \ell_\infty$ is therefore a linear subspace, and $T: X \to T(X)$ is a bijective linear isometry. Thus $X$ is isometrically isomorphic to the subspace $T(X) \subseteq \ell_\infty$, completing the proof.
[/step]
