Description: A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | trgring | ⊢ ( 𝑅 ∈ TopRing → 𝑅 ∈ Ring ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) | |
2 | 1 | istrg | ⊢ ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ TopMnd ) ) |
3 | 2 | simp2bi | ⊢ ( 𝑅 ∈ TopRing → 𝑅 ∈ Ring ) |