Metamath Proof Explorer

Theorem nrgtgp

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

Ref Expression
Assertion nrgtgp 
|- ( R e. NrmRing -> R e. TopGrp )

Proof

Step Hyp Ref Expression
1 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
2 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
3 ringabl 
 |-  ( R e. Ring -> R e. Abel )
4 2 3 syl 
 |-  ( R e. NrmRing -> R e. Abel )
5 ngptgp 
 |-  ( ( R e. NrmGrp /\ R e. Abel ) -> R e. TopGrp )
6 1 4 5 syl2anc 
 |-  ( R e. NrmRing -> R e. TopGrp )