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	|- G = ( mulGrp ` R )
Assertion	iscrng	|- ( R e. CRing <-> ( R e. Ring /\ G e. CMnd ) )

Proof

Step	Hyp	Ref	Expression
1		ringmgp.g	|- G = ( mulGrp ` R )
2		fveq2	|- ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
3	2 1	eqtr4di	|- ( r = R -> ( mulGrp ` r ) = G )
4	3	eleq1d	|- ( r = R -> ( ( mulGrp ` r ) e. CMnd <-> G e. CMnd ) )
5		df-cring	|- CRing = { r e. Ring | ( mulGrp ` r ) e. CMnd }
6	4 5	elrab2	|- ( R e. CRing <-> ( R e. Ring /\ G e. CMnd ) )