Direct proof of the separation theorem of Hahn-Banach The "extension" (or "analytic") form of the theorem of Hahn-Banach has a natural and yet elegant proof. In just any textbook I have ever seen, it is proved first; the "separation" (or "geometric") version of Hahn-Banach's theorem is proved as a kind of corollary of the former.
Question: Are the two theorems actually equivalent? If so, is any direct proof of the analytic version known that is instead based on the geometric one?
 A: The separating version is ubiquitous in economics, and in my experience, most textbooks in mathematical economics prove it directly (though sometimes only in the finite dimensional case).
A: Yes, the two theorems are equivalent in the sense that one can easily be deduced from the other and both have direct proofs from scratch.
A standard textbook starting with a direct proof of the geometric version is Schaefer's Topological Vector Spaces, Chapter II, Section 3.
The statement Schaefer proves is:

Let $F$ be a subspace of a topological vector space $E$ and let $U$ be a nonempty open convex subset, disjoint from $F$. Then there is a closed hyperplane $H$ containing $F$ and disjoint from $U$.

The usual reductions via translation and taking the difference of the convex sets then yield the separation theorems of an open convex set from a point and of an open convex set from a compact convex set.

The proof starts by a simple geometric observation: Let $U$ be an open and convex subset of a Hausdorff topological vector space of dimension $\geq 2$. If $U$ does not contain $0$, then there is a one-dimensional subspace disjoint from $U$. This is easily reduced to the two-dimensional case, where it is rather clear.
To establish the above statement, a straightforward application of Zorn's lemma shows that there is a maximal (hence closed) subspace $M$ containing $F$ and disjoint from $U$. Since $U$ is non-empty, $E/M$ has dimension at least $1$. If the dimension of $E/M$ is $1$, then $M$ is a hyperplane and we're done. Suppose towards a contradiction that the dimension is at least $2$. The image of $U$ in $E/M$ does not contain $0$ and is open since the canonical projection $\pi \colon E \to E/M$ is open. Since $M$ is closed, $E/M$ is Hausdorff. Therefore there is a one-dimensional subspace $L$ of $E/M$ not meeting the image of $U$. The pre-image of $L$ contains $M$, is strictly larger and does not meet $U$, contradicting the maximality of $M$.

In order to get the analytic form, identify a linear functional on a subspace with its graph in $E \times \mathbb{R}$. Endow $E \times \mathbb{R}$ with the product topology induced by the sublinear functional $p$ and the usual topology on $\mathbb{R}$. The set $U = \lbrace (x,t) \mid p(x) \lt t\rbrace$ is an open convex cone in $E \times \mathbb{R}$, not containing $(0,0)$. A linear functional $f$ is dominated by $p$ iff $\operatorname{graph}(f)$ is disjoint from $U$. A maximal closed hyperplane $M$ containing $\operatorname{graph}(f)$ and disjoint from $U$ is then seen to be the graph of a linear functional $F$ which is obviously an extension of $f$ and dominated by $p$.
