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 ∈ NrmRing → R ∈ TopGrp

Proof

Step Hyp Ref Expression
1 nrgngp ⊢ R ∈ NrmRing → R ∈ NrmGrp
2 nrgring ⊢ R ∈ NrmRing → R ∈ Ring
3 ringabl ⊢ R ∈ Ring → R ∈ Abel
4 2 3 syl ⊢ R ∈ NrmRing → R ∈ Abel
5 ngptgp ⊢ R ∈ NrmGrp ∧ R ∈ Abel → R ∈ TopGrp
6 1 4 5 syl2anc ⊢ R ∈ NrmRing → R ∈ TopGrp