This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) )