Metamath Proof Explorer

Theorem ngpxms

Description: A normed group is an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion ngpxms 
|- ( G e. NrmGrp -> G e. *MetSp )

Proof

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