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 M = mulGrp R
Assertion trgtmd R TopRing M TopMnd

Proof

Step Hyp Ref Expression
1 istrg.1 M = mulGrp R
2 1 istrg R TopRing R TopGrp R Ring M TopMnd
3 2 simp3bi R TopRing M TopMnd