Theorem: Hahn-Banach Theorem/Complex Vector Space

Let $X$ be a vector space over $\C$. 
Let $p : X \to \R$ be a seminorm on $X$. 
Let $X_0$ be a linear subspace of $X$. 
Let $f_0 : X_0 \to \C$ be a linear functional such that: 
:$\cmod {\map {f_0} x} \le \map p x$ for each $x \in X_0$.
Then there exists a linear functional $f$ defined on the whole space $X$ which extends $f_0$ and satisfies: 
:$\cmod {\map f x} \le \map p x$ for each $x \in X$.
That is, there exists a linear functional $f : X \to \C$ such that: 
:$\cmod {\map f x} \le \map p x$ for each $x \in X$
and:
:$\map f x = \map {f_0} x$ for each $x \in X_0$.

Proof:
{{Explain|Missing reference to the use of Boolean Prime Ideal Theorem/Ultrafilter Lemma or Axiom of Choice/Zorn's Lemma}}
Define $g_0 : X_0 \to \R$ by: 
:$\map {g_0} x = \map \Re {\map {f_0} x}$
for each $x \in X_0$.
By Real Part of Linear Functional is Linear Functional, $g_0$ is an $\R$-linear functional.
Also, define $h_0 : X_0 \to \R$ by: 
:$\map {h_0} x = \map \Im {\map {f_0} x}$ 
for each $x \in X$. 
By Imaginary Part of Linear Functional is Linear Functional, $h_0$ is an $\R$-linear functional.
Now, for each $x \in X$, we have: 
{{begin-eqn}}
{{eqn	| l = \cmod {\map {g_0} x}
		| r = \sqrt {\paren {\map {g_0} x}^2}
}}
{{eqn	| o = \le
		| r = \sqrt {\paren {\map {g_0} x}^2 + \paren {\map {h_0} x}^2}
}}
{{eqn	| r = \cmod {\map {f_0} x}
}}
{{eqn	| o = \le
		| r = \map p x
}}
{{end-eqn}}
Let $X_\R$ be the realification of $X$.
By Hahn-Banach Theorem: Real Vector Space on $X_\R$, there exists a $\R$-linear functional $g : X \to \R$ extending $g_0$ and satisfying: 
:$\cmod {\map g x} \le \map p x$ 
for each $x \in X$. 
Define $f : X \to \C$ by: 
:$\map f x = \map g x - i \map g {i x}$
for each $x \in X$. 
From Real Linear Functional is Real Part of Unique Linear Functional, we have that: 
:$f : X \to \C$ is a linear functional
and: 
:$\map g x = \map \Re {\map f x}$
for each $x \in X$. 
We now want to show that $f$ extends $f_0$.
Let $F_0$ be the restriction of $f$ to $X_0$.
We want to show that:
:$f_0 = F_0$
We have:
:$\map \Re {\map f x} = \map g x$
for each $x \in X$.
Hence: 
:$\map \Re {\map f x} = \map {g_0} x = \map \Re {\map {f_0} x}$ 
for each $x \in X_0$. 
So: 
:$\map \Re {\map {F_0} x} = \map \Re {\map {f_0} x}$
for each $x \in X_0$.
From Linear Functional on Complex Vector Space is Uniquely Determined by Real Part, it follows that: 
:$\map {F_0} x = \map {f_0} x$
for each $x \in X_0$.
So $f$ indeed extends $f_0$.
Now take $x \in X$. 
Pick $\lambda \in \C$ such that:
:$\cmod \lambda = 1$
and: 
:$\lambda \map f x = \cmod {\map f x}$ 
Then, since $f$ is $\C$-linear: 
{{begin-eqn}}
{{eqn	| l = \cmod {\map f x}
		| r = \lambda \map f x
}}
{{eqn	| r = \map f {\lambda x}
}}
{{eqn	| r = \map g {\lambda x} - i \map g {i \lambda x}
}}
{{end-eqn}}
Since: 
:$\cmod {\map f x} \in \R$
we have that:
:$\map g {i \lambda x} = 0$ 
Finally, we have: 
{{begin-eqn}}
{{eqn	| l = \cmod {\map f x}
		| r = \map g {\lambda x}
}}
{{eqn	| o = \le
		| r = \map p {\lambda x}
}}
{{eqn	| r = \cmod \lambda \map p x
		| c = {{Template:SeminormAxiom|2}}
}}
{{eqn	| r = \map p x
}}
{{end-eqn}}
So $f$ is a linear functional satisfying our requirements.
{{qed}}
{{Namedfor|Hans Hahn|name2 = Stefan Banach}}