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 )