Metamath Proof Explorer

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 \in CRing \leftrightarrow (R \in Ring \land G \in CMnd)$

Step	Hyp	Ref	Expression
1		ringmgp.g	$⊢ G = {mulGrp}_{R}$
2		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
3	2 1	eqtr4di	$⊢ r = R \to {mulGrp}_{r} = G$
4	3	eleq1d	$⊢ r = R \to ({mulGrp}_{r} \in CMnd \leftrightarrow G \in CMnd)$
5		df-cring	$⊢ CRing = \{r \in Ring \| {mulGrp}_{r} \in CMnd\}$
6	4 5	elrab2	$⊢ R \in CRing \leftrightarrow (R \in Ring \land G \in CMnd)$