Theorem crngmgp

Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypothesis	ringmgp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		ringmgp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2	1	iscrng	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd ) )
3	2	simprbi	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )