The following is Theorem V.1 in Reed & Simon's book on functional analysis.
Let $V$ be a vector space with a Hausdorff topology in which addition and scalar multiplication are separately continuous. Then $V$ is a locally convex space if and only if $0$ has a neighborhood base of balanced, convex, absorbing sets.
In their proof they reference the following lemma about the Minkowski functional or gauge of an absorbing set $C$ with the additional property that if $x \in C$ and $0 \leq t \leq 1$, then $tx \in C$.
(a) If $t \geq 0$, then $\rho(tx) = t \rho(x)$ for the gauge of any set $C$.
(b) $\rho$ obeys $\rho(x + y) \leq \rho(x) + \rho(y)$ if $C$ is convex.
(c) $\rho$ obeys $\rho(\lambda x) = |\lambda| \rho(x)$ if $C$ is circled/balanced.
(d) $\{x | \rho(x) < 1 \} \subset C \subset \{x | \rho(x) \leq 1\}$.
Their proof of Theorem V.1 is:
Let $\mathscr{U}$ be a neighborhood base at $0$ containing only convex, balanced, absorbing sets; for each $U \in \mathscr{U}$, let $\rho_U$ be the gauge of $U$. By (b) and (c) of the lemma, $\rho$ is a seminorm and by (d) the neighborhoods of $0$ in the original topology are the same as those in the locally convex topology given by the seminorms $\{\rho_U | U \in \mathscr{U}\}$. Since addition is separately continuous in both topologies, the neighborhood about any point are identical in the two topologies.
I have three questions about their proof:
- How do we know that such a neighborhood base about $0$ exists?
- How does it follow from (d) that the neighborhoods of $0$ in the original topology are the same as those in the locally convex topology given by the seminorms $\{\rho_U | U \in \mathscr{U}\}$?
- I do not see how the proof sufficiently proves the forward direction, that if $V$ is locally convex then $0$ has a neighborhood base of balanced, convex, and absorbing sets. It seems to me that we have only proved this for locally convex spaces induced by a particular family of seminorms, but not in full generality.