Theorem iscrng

Description: A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypothesis	ringmgp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion	iscrng	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd ) )

Proof

Step	Hyp	Ref	Expression
1		ringmgp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2		fveq2	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
3	2 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝐺 )
4	3	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ CMnd ↔ 𝐺 ∈ CMnd ) )
5		df-cring	⊢ CRing = { 𝑟 ∈ Ring ∣ ( mulGrp ‘ 𝑟 ) ∈ CMnd }
6	4 5	elrab2	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd ) )