Theorem 8.2.6 (Metrisability of Topological Vector Spaces). Let $E$ be a TVS over $K \in \RC$, then the following are equivalent:
There exists a pseudonorm that induces the topology on $E$.
There exists a translation-invariant pseudometric that induces the topology on $E$.
$E$ admits a countable fundamental system of entourages.
There exists a pseudometric that induces the topology on $E$.
$E$ admits a countable fundamental system of neighbourhoods at $0$.
Proof. (3) $\Rightarrow$ (4): By Theorem 5.3.12.
(4) $\Rightarrow$ (1): By Proposition 8.1.11, there exists $\seq{U_n}\subset \cn_{E}(0)$ circled and radial such that for each $n \in \natp$, $U_{n+1}+ U_{n+1}\subset U_{n}$. By Lemma 8.2.4, there exists a pseudonorm $\rho: E \to [0, \infty)$ such that for each $N \in \natp$, $U_{n+1}\subset \rho^{-1}([0, 2^{-n})) \subset U_{n}$. In which case, $\rho$ induces the topology on $E$.$\square$