Proof of Norming Functionals in a Separable Real Normed Space, and the Dual Separates Points

We first treat a point $x\neq0_{X}$ and construct $F\in X^{*}$ with $\lVert F\rVert_{*}=1$ and $F(x)=\lVert x\rVert$. The norm is a sublinear functional on $X$ by Elementary Properties of Sublinear Functionals (iv), and

$$-\lVert -x\rVert\le\lVert x\rVert\le\lVert x\rVert,$$

because $\lVert -x\rVert=\lVert(-1)x\rVert=\lVert x\rVert$ by Elementary Identities in a Vector Space (iv) and Norms and Real Normed Spaces (iii). So A Dominated Linear Functional on a Line (i) and A Dominated Linear Functional on a Line (ii), applied with $p=\lVert\cdot\rVert$, $x_{0}=x$ and $c=\lVert x\rVert$, give the linear subspace $\mathbb{R}x$ of $X$ and the linear functional $f$ on it with $f(tx)=t\lVert x\rVert$ for $t\in\mathbb{R}$ and $f\le\lVert\cdot\rVert$ on $\mathbb{R}x$. By The Hahn–Banach Theorem in a Separable Real Normed Space (i), applied with $p=\lVert\cdot\rVert$, the constant $1$ and $f$ on $\mathbb{R}x$, there is $F\in X^{*}$ with $F=f$ on $\mathbb{R}x$ and $F\le\lVert\cdot\rVert$ on $X$; in particular, as $x=1x$ (Vector Space over a Field (vi)),

$$F(x)=f(1x)=\lVert x\rVert .$$

By Elementary Properties of Sublinear Functionals (vi) (with $M=X$ and $C=1$), $|F(y)|\le\lVert y\rVert$ for every $y\in X$, so $1\in B_{F}$ by Bounded Linear Functionals and the Dual Space of a Real Normed Space (ii). The dual norm is $\lVert F\rVert_{*}=\inf B_{F}$ and an infimum is a lower bound (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)), so $\lVert F\rVert_{*}\le1$. Conversely, The Nonnegative Bounds of a Bounded Linear Functional Have an Infimum, Which Is a Bound (ii) gives $\lVert x\rVert=F(x)\le\lVert F\rVert_{*}\lVert x\rVert$, and $\lVert x\rVert>0$ by Norms and Real Normed Spaces (i) and Norms and Real Normed Spaces (ii); dividing by $\lVert x\rVert$ gives $\lVert F\rVert_{*}\ge1$. Hence $\lVert F\rVert_{*}=1$.

For $x=0_{X}$, the zero functional on $X$ is linear (Linear Functional on a Linear Subspace (iii)) and has the bound $0$, so it lies in $X^{*}$ by Bounded Linear Functionals and the Dual Space of a Real Normed Space (iii) and Bounded Linear Functionals and the Dual Space of a Real Normed Space (iv). Its dual norm is at most $1$, as $1$ lies in its set of nonnegative bounds (Bounded Linear Functionals and the Dual Space of a Real Normed Space (ii)), and its value at $0_{X}$ is $0=\lVert0_{X}\rVert$ by The Norm Metric of a Real Normed Space (i). Together with the case $x\neq0_{X}$, this proves (i).

For (ii), suppose $X\neq\{0_{X}\}$. For $x\neq0_{X}$ the functional constructed above will do. For $x=0_{X}$, fix a point $y\neq0_{X}$ of $X$ and let $F$ be the functional constructed above for $y$. Then $\lVert F\rVert_{*}=1$, and

$$F(0_{X})=F(0\cdot0_{X})=0\cdot F(0_{X})=0=\lVert0_{X}\rVert$$

by Elementary Identities in a Vector Space (ii), Linear Functional on a Linear Subspace (ii) and The Norm Metric of a Real Normed Space (i).

For (iii), let $x\neq y$. Then $x-y\neq0_{X}$, since $x-y=0_{X}$ would give $x=y+(x-y)=y$ (Elementary Identities in a Vector Space (viii)). Let $F$ be the functional constructed above for $x-y$. By Linear Functional on a Linear Subspace (i), Linear Functional on a Linear Subspace (ii) and Norms and Real Normed Spaces (ii),

$$F(x)-F(y)=F(x-y)=\lVert x-y\rVert>0,$$

so $F(x)\neq F(y)$.