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 \in TopRing \to M \in TopMnd$

Step	Hyp	Ref	Expression
1		istrg.1	$⊢ M = {mulGrp}_{R}$
2	1	istrg	$⊢ R \in TopRing \leftrightarrow (R \in TopGrp \land R \in Ring \land M \in TopMnd)$
3	2	simp3bi	$⊢ R \in TopRing \to M \in TopMnd$