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 e. TopRing -> M e. TopMnd )

Proof

Step	Hyp	Ref	Expression
1		istrg.1	|- M = ( mulGrp ` R )
2	1	istrg	|- ( R e. TopRing <-> ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) )
3	2	simp3bi	|- ( R e. TopRing -> M e. TopMnd )