Topological Groups and Families of Pseudometrics The topology on a topological group is generated by a family of pseudometrics.  The only proof I know passes through uniform spaces (by which I mean the entourage definition): A topological group has a uniformity and by a theorem of Weil, every uniformity comes from a family of pseudometrics.  Is there a direct construction of the pseudometrics that bypasses Weil's theorem?
 A: The basic strategy should consist of two steps: (1) topological groups are completely regular, and (2) completely regular spaces are subspaces of products of pseudometric spaces. Of course, this is not hugely different from the proof which passes through uniform structures, but certainly you can bypass that language. 
Both parts are in some sense classical. If you have Munkres close to hand, then the proof of (1) can be extracted by following the recipe given in exercise 5 on page 237. (Yes, he states it for the $T_0$/Hausdorff case, but the proof goes through without that assumption.) 
A space $X$ is completely regular iff its Kolmogorov quotient $X_h$ is completely regular (i.e., Tychonoff -- see here), and a Tychonoff space embeds in a product of copies of the unit interval (Munkres, p. 237, theorem 2.2). In this way, the topology of $X_h$ is generated by a family of metrics, and by pulling back these metrics along the quotient map $X \to X_h$, one gets a generating family of pseudometrics for $X$. 
Edit: As for arsmath's question in the comment below, one may refer to Hewitt and Ross's Abstract Harmonic Analysis (as mentioned by Theo Buehler in his comment above), p. 67 ff. (link). See in particular theorem 8.2 (page 68), where the direct construction of the pseudometrics gives a uniformity which coincides with the left uniformity of the topological group. 
