Metamath Proof Explorer

Theorem nrgring

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

Ref Expression
Assertion nrgring 
|- ( R e. NrmRing -> R e. Ring )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( norm ` R ) = ( norm ` R )
2 eqid 
 |-  ( AbsVal ` R ) = ( AbsVal ` R )
3 1 2 nrgabv 
 |-  ( R e. NrmRing -> ( norm ` R ) e. ( AbsVal ` R ) )
4 2 abvrcl 
 |-  ( ( norm ` R ) e. ( AbsVal ` R ) -> R e. Ring )
5 3 4 syl 
 |-  ( R e. NrmRing -> R e. Ring )