Metamath Proof Explorer

Theorem ringcom

Description: Commutativity of the additive group of a ring. (See also lmodcom .) (Contributed by Steve Rodriguez, 9-Sep-2007) This theorem followed originally from the definition immediately, but now is derived from other properties of a ring. This proof requires the existence of a multiplicative identity, and the existence of additive inverses. Therefore, this proof is not applicable for semirings. (Revised by Gérard Lang, 4-Dec-2014) (Proof shortened by AV, 1-Feb-2025)

Ref Expression
Hypotheses ringacl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringacl.p ⊢ + = ( +g ‘ 𝑅 )
Assertion ringcom ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ringacl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringacl.p ⊢ + = ( +g ‘ 𝑅 )
3 1 2 ringcomlem ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
4 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
5 4 ringgrpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Grp )
6 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + 𝑋 ) ∈ 𝐵 )
8 4 6 6 7 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑋 ) ∈ 𝐵 )
9 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
10 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
11 5 8 9 9 10 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
12 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
13 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
14 5 12 6 9 13 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
15 3 11 14 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) )
16 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝐵 )
17 4 8 9 16 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝐵 )
18 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝐵 )
19 4 12 6 18 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝐵 )
20 1 2 grprcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝐵 ∧ ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) ↔ ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) ) )
21 5 17 19 9 20 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) ↔ ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) ) )
22 15 21 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) )
23 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
24 5 6 6 9 23 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
25 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
26 5 6 9 6 25 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
27 22 24 26 3eqtr3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
28 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
29 28 3com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
30 1 2 grplcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
31 5 12 29 6 30 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
32 27 31 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )