Relative separation of an open convex set from an exterior point

Fix $c_0\in C$, set $U=C-c_0$ and $v=z-c_0$. Then $0\in U$ and $v\mathrm{\notin }U$, hence $v\mathrm{\ne }0$. If $u_j=c_j-c_0\in U$ and $0\le t\le 1$, then $(1-t)u_1+t{u}_2=((1-t)c_1+t{c}_2)-c_0\in U$. A ball in $C$ about $c$ translates to a ball of the same radius in $U$ about $c-c_0$, so $U$ is open. Fix $r>0$ with $B(0,r)\subseteq U$.

Let $p=p_U$. Its gauge is finite and sublinear on the underlying real space, nonnegative everywhere, and bounded above by $\mathrm{\parallel }x\mathrm{\parallel }\mathrm{/}r$. Because $v\mathrm{\notin }U=\{p<1\}$, $p(v)\ge 1$.

The set $M=\mathbb{R}v$ is a real linear subspace. Since $v\mathrm{\ne }0$, $tv$ has a unique real coefficient $t$, and $g(tv)=t$ defines a real-linear functional. For $t\ge 0$, $g(tv)=t\le tp(v)=p(tv)$; for $t<0$, $g(tv)=t<0\le p(tv)$. This checks domination on every element of M, including zero.

Applying relative dominated extension on the underlying real $X$ gives real-linear $F$ extending $g$ and satisfying $-p(-x)\le F(x)\le p(x)$. The two gauge upper bounds imply $-\mathrm{\parallel }x\mathrm{\parallel }\mathrm{/}r\le F(x)\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{/}r$, so $\mathrm{\mid }F(x)\mathrm{\mid }\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{/}r$. Also $F(v)=1$.

Over $\mathbb{R}$ put $f=F$. Over $\mathbb{C}$ put $f(x)=F(x)-iF(ix)$; reconstruction gives complex linearity and real part $F$, and $\mathrm{\mid }f(x)\mathrm{\mid }\le \mathrm{\mid }F(x)\mathrm{\mid }+\mathrm{\mid }F(ix)\mathrm{\mid }\le 2\mathrm{\parallel }x\mathrm{\parallel }\mathrm{/}r$. Thus in either field $f\in X^{\ast }$, and it is nonzero because $\mathrm{Re}f(v)=1$. The explicit bounds give continuity: $\mathrm{\mid }f(x)-f(y)\mathrm{\mid }\le (2\mathrm{/}r)\mathrm{\parallel }x-y\mathrm{\parallel }$ in both cases.

For every $c\in C$, $c-c_0\in U$, so $F(c-c_0)\le p(c-c_0)<1=F(z-c_0)$. Adding $F(c_0)$ gives $\mathrm{Re}f(c)=F(c)<F(z)=\mathrm{Re}f(z)$, as required.