Metamath Proof Explorer


Theorem ngptps

Description: A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion ngptps
|- ( G e. NrmGrp -> G e. TopSp )

Proof

Step Hyp Ref Expression
1 ngpms
 |-  ( G e. NrmGrp -> G e. MetSp )
2 mstps
 |-  ( G e. MetSp -> G e. TopSp )
3 1 2 syl
 |-  ( G e. NrmGrp -> G e. TopSp )