Metamath Proof Explorer

Theorem nrgngp

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

Ref Expression
Assertion nrgngp 
|- ( R e. NrmRing -> R e. NrmGrp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( norm ` R ) = ( norm ` R )
2 eqid 
 |-  ( AbsVal ` R ) = ( AbsVal ` R )
3 1 2 isnrg 
 |-  ( R e. NrmRing <-> ( R e. NrmGrp /\ ( norm ` R ) e. ( AbsVal ` R ) ) )
4 3 simplbi 
 |-  ( R e. NrmRing -> R e. NrmGrp )