Proof of Separating a Point from an Open Convex Set in a Separable Real Normed Space

We translate $C$ to a neighbourhood of the origin, separate with its gauge, and translate back.

Fix $c_{0}\in C$, and let

$$U=\{x-c_{0}:x\in C\},\qquad y_{0}=x_{0}-c_{0}.$$

The set $U$ is convex: for $x,x'\in C$ and $0\le t\le1$,

$$t(x-c_{0})+(1-t)(x'-c_{0})=\bigl(tx+(1-t)x'\bigr)-c_{0}$$

by Elementary Identities in a Vector Space (ix), Elementary Identities in a Vector Space (vi), Vector Space over a Field (i), Vector Space over a Field (ii), Vector Space over a Field (viii) and Vector Space over a Field (vi) (with $tc_{0}+(1-t)c_{0}=c_{0}$), and $tx+(1-t)x'\in C$ by Convex Subset of a Real Vector Space (i). The set $U$ is open (Open Subset of a Metric Space (i)). Here we use that $(u+w)-(v+w)=u-v$ and $(u+w)-w=u$ for $u,v,w\in X$ (The Zero Vector, Negatives and Differences in a Vector Space (iii), Elementary Identities in a Vector Space (vi), Elementary Identities in a Vector Space (vii), The Zero Vector, Negatives and Differences in a Vector Space (i), Vector Space over a Field (i), Vector Space over a Field (ii)). Let $x\in C$ and $\rho>0$ with $B(x,\rho)\subseteq C$, and let $z\in B(x-c_{0},\rho)$. By The Norm Metric of a Real Normed Space (i), Elementary Identities in a Vector Space (viii) and Open Ball in a Metric Space (ii),

$$d_{X}(x,z+c_{0})=\bigl\lVert\bigl((x-c_{0})+c_{0}\bigr)-(z+c_{0})\bigr\rVert=\lVert(x-c_{0})-z\rVert=d_{X}(x-c_{0},z)<\rho ,$$

so $z+c_{0}\in B(x,\rho)\subseteq C$, and therefore $z=(z+c_{0})-c_{0}\in U$. Hence $B(x-c_{0},\rho)\subseteq U$. Moreover $0_{X}=c_{0}-c_{0}\in U$ (Elementary Identities in a Vector Space (vii)). Finally $y_{0}\notin U$ and $y_{0}\neq0_{X}$: if $y_{0}=x-c_{0}$ with $x\in C$, or $y_{0}=0_{X}$, then Elementary Identities in a Vector Space (viii) gives $x_{0}=x\in C$, respectively $x_{0}=c_{0}\in C$, contradicting $x_{0}\notin C$.

Let $p=p_{U}$ be the gauge of $U$. It is a sublinear functional by Properties of the Minkowski Gauge (i). Fix $r>0$ with $B(0_{X},r)\subseteq U$ (The Scaling Set of an Open Convex Neighbourhood of the Origin Has an Infimum (i)); then

$$0\le p(x)\le r^{-1}\lVert x\rVert\qquad\text{for every }x\in X$$

by Properties of the Minkowski Gauge (ii). Since $y_{0}\notin U$, Properties of the Minkowski Gauge (iii) gives $p(y_{0})\ge1$.

Thus $y_{0}\neq0_{X}$ and $-p(-y_{0})\le0\le1\le p(y_{0})$. So A Dominated Linear Functional on a Line (i) and A Dominated Linear Functional on a Line (ii), applied with $x_{0}=y_{0}$ and $c=1$, give the linear subspace $G=\mathbb{R}y_{0}$ of $X$ and the linear functional $g$ on $G$ with $g(ty_{0})=t$ for every $t\in\mathbb{R}$ and $g\le p$ on $G$. By The Hahn–Banach Theorem in a Separable Real Normed Space (i), applied to $p$ with the constant $r^{-1}$ and to $g$ on $G$, there is $F\in X^{*}$ with $F=g$ on $G$ and $F\le p$ on $X$; in particular $F(y_{0})=g(1y_{0})=1$, as $y_{0}=1y_{0}$ (Vector Space over a Field (vi)).

Now let $x\in C$. Then $x-c_{0}\in U$, so $p(x-c_{0})<1$ by Properties of the Minkowski Gauge (iii), and by Linear Functional on a Linear Subspace (i) and Linear Functional on a Linear Subspace (ii)

$$F(x)-F(c_{0})=F(x-c_{0})\le p(x-c_{0})<1=F(y_{0})=F(x_{0})-F(c_{0}).$$

Hence $F(x)<F(x_{0})$, which proves (i).