Metamath Proof Explorer


Theorem trgring

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

Ref Expression
Assertion trgring ( 𝑅 ∈ TopRing → 𝑅 ∈ Ring )

Proof

Step Hyp Ref Expression
1 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
2 1 istrg ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ TopMnd ) )
3 2 simp2bi ( 𝑅 ∈ TopRing → 𝑅 ∈ Ring )