Metamath Proof Explorer

Theorem ngpgrp

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

Ref Expression
Assertion ngpgrp 
|- ( G e. NrmGrp -> G e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( norm ` G ) = ( norm ` G )
2 eqid 
 |-  ( -g ` G ) = ( -g ` G )
3 eqid 
 |-  ( dist ` G ) = ( dist ` G )
4 1 2 3 isngp 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( ( norm ` G ) o. ( -g ` G ) ) C_ ( dist ` G ) ) )
5 4 simp1bi 
 |-  ( G e. NrmGrp -> G e. Grp )