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

Metamath Proof Explorer

Theorem trgtmd

Description: The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypothesis istrg.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion trgtmd ( 𝑅 ∈ TopRing → 𝑀 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 istrg.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 1 istrg ⊢ ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd ) )
3 2 simp3bi ⊢ ( 𝑅 ∈ TopRing → 𝑀 ∈ TopMnd )