Proof of The Hahn–Banach Theorem in a Separable Real Normed Space

We extend $f$ step by step along a dense sequence and then pass to $X$ by continuity. One enumeration of a dense set is fixed and every step is canonical, so no choice is used.

A dense sequence. Since $X$ is separable (Separable Metric Space and Separable Real Normed Space (ii), Separable Metric Space and Separable Real Normed Space (i)), we fix a countable set $D\subseteq X$ that is dense in $(X,d_{X})$. It is nonempty, because by Dense Subset of a Metric Space (i) the ball $B(0_{X},1)$ meets $D$. So by Countable Set (i) we may fix a surjective function $e:\mathbb{N}\to D$.

Extending along the sequence. Let $\mathcal{A}$ be the set of pairs $(W,g)$ such that $W$ is a linear subspace of $X$ containing $M$ and $g$ is a linear functional on $W$ with $g=f$ on $M$ and $g\le p$ on $W$ (a set, being a subset of $\mathcal{P}(X)\times\mathcal{P}(X\times\mathbb{R})$). The pair $(M,f)$ lies in $\mathcal{A}$. Define $\Phi:\mathbb{N}\times\mathcal{A}\to\mathcal{A}$ by

$$\Phi\bigl(k,(W,g)\bigr)=\begin{cases}(W,g)&\text{if }e(k)\in W,\\ (W+\mathbb{R}e(k),\tilde g)&\text{if }e(k)\notin W,\end{cases}$$

where, in the second case, $\tilde g$ is the function on $W+\mathbb{R}e(k)$ given by One-Step Extension of a Dominated Linear Functional (iv) for the subspace $W$, the point $x_{0}=e(k)$ and the functional $g$, built with the supremum $c$ of One-Step Extension of a Dominated Linear Functional (iii). By One-Step Extension of a Dominated Linear Functional (i) and One-Step Extension of a Dominated Linear Functional (iv), $W+\mathbb{R}e(k)$ is a linear subspace containing $W$, hence $M$, and $\tilde g$ is a linear functional on it that agrees with $g$ on $W$, hence with $f$ on $M$, and is dominated by $p$; so the value lies in $\mathcal{A}$ (and $\Phi$, given explicitly, is a function).

By Recursion on the Natural Numbers Starting at One (i), applied with the set $\mathcal{A}$, the starting value $(M,f)$ and the step $\Phi$, there is a function $k\mapsto(W_{k},g_{k})$ on $\mathbb{N}$ with

$$(W_{1},g_{1})=(M,f),\qquad (W_{k+1},g_{k+1})=\Phi\bigl(k,(W_{k},g_{k})\bigr)\quad(k\in\mathbb{N}).$$

In both cases of the definition of $\Phi$ we have $W_{k}\subseteq W_{k+1}$, $g_{k+1}=g_{k}$ on $W_{k}$ and $e(k)\in W_{k+1}$ (in the second case by One-Step Extension of a Dominated Linear Functional (i) and One-Step Extension of a Dominated Linear Functional (iv)). By induction on $k$ (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)), $W_{j}\subseteq W_{k}$ and $g_{k}=g_{j}$ on $W_{j}$ whenever $j\le k$.

The union. Let $M_{\infty}=\bigcup_{k\in\mathbb{N}}W_{k}$, and for $x\in M_{\infty}$ let $f_{\infty}(x)=g_{k}(x)$ for any $k$ with $x\in W_{k}$; by the nesting this does not depend on $k$ (so $f_{\infty}$ is the union of the graphs of the $g_{k}$). Any two points of $M_{\infty}$ lie in a common $W_{k}$, so $M_{\infty}$ is a linear subspace of $X$ (Linear Subspace of a Real Vector Space (iv)), and $f_{\infty}$ is a linear functional on $M_{\infty}$ with $f_{\infty}=f$ on $M$ and $f_{\infty}\le p$ on $M_{\infty}$. Since $e$ is surjective and $e(k)\in W_{k+1}$ for every $k$, we have $D\subseteq M_{\infty}$; hence $M_{\infty}$ is dense in $(X,d_{X})$ by Dense Subset of a Metric Space (i).

Extension to $X$. By Elementary Properties of Sublinear Functionals (vi), applied to the subspace $M_{\infty}$ and the functional $f_{\infty}$, we have $|f_{\infty}(x)|\le C\lVert x\rVert$ for $x\in M_{\infty}$. With Linear Functional on a Linear Subspace (i) and Linear Functional on a Linear Subspace (ii) this gives, for $x,y\in M_{\infty}$,

$$|f_{\infty}(x)-f_{\infty}(y)|=|f_{\infty}(x-y)|\le C\lVert x-y\rVert=C\,d_{X}(x,y)$$

(The Norm Metric of a Real Normed Space (i)). So Lipschitz Extension of a Real Function from a Subset of a Metric Space (i), applied in $(X,d_{X})$ to the subset $M_{\infty}$ (nonempty, as $0_{X}\in M$), the function $f_{\infty}$ and $L=C$, yields a function $F:X\to\mathbb{R}$ with $F=f_{\infty}$ on $M_{\infty}$ and

$$|F(x)-F(y)|\le C\lVert x-y\rVert\qquad\text{for all }x,y\in X.$$

$F$ is linear. Let $x,y\in X$ and $\lambda\in\mathbb{R}$, and let $\varepsilon>0$. Once $\varepsilon$ is fixed, the density of $M_{\infty}$ provides $m_{1}\in M_{\infty}$ with $\lVert x-m_{1}\rVert<\varepsilon$ and $m_{2}\in M_{\infty}$ with $\lVert y-m_{2}\rVert<\varepsilon$. Since $F=f_{\infty}$ on $M_{\infty}$ and $f_{\infty}$ is linear, $F(m_{1}+m_{2})=F(m_{1})+F(m_{2})$ and $F(\lambda m_{1})=\lambda F(m_{1})$. The Lipschitz estimate for $F$, Norms and Real Normed Spaces (iv) and Norms and Real Normed Spaces (iii) then give

$$|F(x+y)-F(x)-F(y)|\le|F(x+y)-F(m_{1}+m_{2})|+|F(m_{1})-F(x)|+|F(m_{2})-F(y)|\le4C\varepsilon,$$ $$|F(\lambda x)-\lambda F(x)|\le|F(\lambda x)-F(\lambda m_{1})|+|\lambda|\,|F(m_{1})-F(x)|\le2C|\lambda|\varepsilon .$$

Since $\varepsilon>0$ was arbitrary, $F(x+y)=F(x)+F(y)$ and $F(\lambda x)=\lambda F(x)$: $F$ is a linear functional on $X$.

$F$ is dominated by $p$. Let $x\in X$ and $\varepsilon>0$, and then pick $m_{1}\in M_{\infty}$ with $\lVert x-m_{1}\rVert<\varepsilon$ as before. By Elementary Properties of Sublinear Functionals (v), $p(m_{1})\le p(x)+C\lVert x-m_{1}\rVert$, so

$$F(x)\le F(m_{1})+C\varepsilon=f_{\infty}(m_{1})+C\varepsilon\le p(m_{1})+C\varepsilon\le p(x)+2C\varepsilon .$$

As $\varepsilon>0$ was arbitrary, $F(x)\le p(x)$.

$F$ is bounded. By Elementary Properties of Sublinear Functionals (vi) with $M=X$ and $f=F$, $|F(x)|\le C\lVert x\rVert$ for every $x\in X$. So $C$ is a bound of $F$ (Bounded Linear Functionals and the Dual Space of a Real Normed Space (i)), $F$ is bounded (Bounded Linear Functionals and the Dual Space of a Real Normed Space (iii)), and $F\in X^{*}$ by Bounded Linear Functionals and the Dual Space of a Real Normed Space (iv). Finally $F=f_{\infty}=f$ on $M$. This proves (i).