I’m pleased to say that I find the derivation of the Hahn-Banach theorem pretty straightforward by now. Let me first state it, for the real case.
Hahn-Banach theorem: Let be a real vector space. Let be sublinear. If be a linear functional on the subspace with for , then there exists a linear extension of to all of (call it ) such that for with for and for all .
To show this, start by taking any . We wish to assign some to that keeps as the dominating function in the vector space . For this to happen, applying the linearity of and the domination constraint, we can derive
This reduces to
Such can be proven via
Now take the space of linear functionals defined on some specific subspace dominated by . Denote an element of it as . We introduce a partial order wherein iff for and . We can apply Zorn’s lemma on this, as we can take the union to derive an upper bound for any chain. Any maximal element is necessarily as if the domain is not the entire vector space, we can by above construct a larger element.