Metamath Proof Explorer

Theorem ringcom

Description: Commutativity of the additive group of a ring. (See also lmodcom .) (Contributed by Gérard Lang, 4-Dec-2014)

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 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
4 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5 1 4 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
6 3 5 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
7 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
8 3 6 6 7 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
9 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 1 2 11 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) = ( ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) ) )
13 3 8 9 10 12 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) = ( ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) ) )
14 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
15 1 2 11 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) ) )
16 3 6 6 14 15 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) ) )
17 13 16 eqtr3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) ) )
18 1 2 11 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) ) )
19 3 6 6 9 18 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) ) )
20 1 11 4 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) = 𝑋 )
21 3 9 20 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) = 𝑋 )
22 21 21 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) ) = ( 𝑋 + 𝑋 ) )
23 19 22 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 𝑋 + 𝑋 ) )
24 1 2 11 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) ) )
25 3 6 6 10 24 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) = ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) ) )
26 1 11 4 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
27 3 10 26 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
28 27 27 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑌 ) ) = ( 𝑌 + 𝑌 ) )
29 25 28 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 𝑌 + 𝑌 ) )
30 23 29 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) + ( ( ( 1r ‘ 𝑅 ) + ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑌 ) ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
31 1 11 4 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
32 3 14 31 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
33 32 32 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑋 + 𝑌 ) ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
34 17 30 33 3eqtr3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
35 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
36 3 35 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Grp )
37 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + 𝑋 ) ∈ 𝐵 )
38 3 9 9 37 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑋 ) ∈ 𝐵 )
39 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
40 36 38 10 10 39 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
41 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
42 36 14 9 10 41 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
43 34 40 42 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) )
44 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝐵 )
45 3 38 10 44 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝐵 )
46 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝐵 )
47 3 14 9 46 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝐵 )
48 1 2 grprcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝐵 ∧ ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) ↔ ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) ) )
49 36 45 47 10 48 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) ↔ ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) ) )
50 43 49 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) )
51 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
52 36 9 9 10 51 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
53 1 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
54 36 9 10 9 53 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
55 50 52 54 3eqtr3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
56 1 2 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
57 56 3com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
58 1 2 grplcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
59 36 14 57 9 58 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
60 55 59 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )