This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrgtgp

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

Ref Expression
Assertion nrgtgp ( 𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp )

Proof

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