Theorem iscrng2

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

	Ref	Expression
Hypotheses	ringcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringcl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	iscrng2	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ringcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringcl.t	⊢ · = ( .r ‘ 𝑅 )
3		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
4	3	iscrng	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ CMnd ) )
5	3	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
6	3 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
7	3 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
8	6 7	iscmn	⊢ ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ↔ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )
9	8	baib	⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )
10	5 9	syl	⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )
11	10	pm5.32i	⊢ ( ( 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ CMnd ) ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )
12	4 11	bitri	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )