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 
|- B = ( Base ` R )
ringacl.p 
|- .+ = ( +g ` R )
Assertion ringcom 
|- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step Hyp Ref Expression
1 ringacl.b 
 |-  B = ( Base ` R )
2 ringacl.p 
 |-  .+ = ( +g ` R )
3 simp1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> R e. Ring )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 1 4 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
6 3 5 syl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( 1r ` R ) e. B )
7 1 2 ringacl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. B /\ ( 1r ` R ) e. B ) -> ( ( 1r ` R ) .+ ( 1r ` R ) ) e. B )
8 3 6 6 7 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( 1r ` R ) .+ ( 1r ` R ) ) e. B )
9 simp2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> X e. B )
10 simp3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> Y e. B )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 1 2 11 ringdi 
 |-  ( ( R e. Ring /\ ( ( ( 1r ` R ) .+ ( 1r ` R ) ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) ( X .+ Y ) ) = ( ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) .+ ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) ) )
13 3 8 9 10 12 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) ( X .+ Y ) ) = ( ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) .+ ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) ) )
14 1 2 ringacl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
15 1 2 11 ringdir 
 |-  ( ( R e. Ring /\ ( ( 1r ` R ) e. B /\ ( 1r ` R ) e. B /\ ( X .+ Y ) e. B ) ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) ( X .+ Y ) ) = ( ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) .+ ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) ) )
16 3 6 6 14 15 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) ( X .+ Y ) ) = ( ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) .+ ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) ) )
17 13 16 eqtr3d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) .+ ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) ) = ( ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) .+ ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) ) )
18 1 2 11 ringdir 
 |-  ( ( R e. Ring /\ ( ( 1r ` R ) e. B /\ ( 1r ` R ) e. B /\ X e. B ) ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) = ( ( ( 1r ` R ) ( .r ` R ) X ) .+ ( ( 1r ` R ) ( .r ` R ) X ) ) )
19 3 6 6 9 18 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) = ( ( ( 1r ` R ) ( .r ` R ) X ) .+ ( ( 1r ` R ) ( .r ` R ) X ) ) )
20 1 11 4 ringlidm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( 1r ` R ) ( .r ` R ) X ) = X )
21 3 9 20 syl2anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( 1r ` R ) ( .r ` R ) X ) = X )
22 21 21 oveq12d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) ( .r ` R ) X ) .+ ( ( 1r ` R ) ( .r ` R ) X ) ) = ( X .+ X ) )
23 19 22 eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) = ( X .+ X ) )
24 1 2 11 ringdir 
 |-  ( ( R e. Ring /\ ( ( 1r ` R ) e. B /\ ( 1r ` R ) e. B /\ Y e. B ) ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) = ( ( ( 1r ` R ) ( .r ` R ) Y ) .+ ( ( 1r ` R ) ( .r ` R ) Y ) ) )
25 3 6 6 10 24 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) = ( ( ( 1r ` R ) ( .r ` R ) Y ) .+ ( ( 1r ` R ) ( .r ` R ) Y ) ) )
26 1 11 4 ringlidm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( ( 1r ` R ) ( .r ` R ) Y ) = Y )
27 3 10 26 syl2anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( 1r ` R ) ( .r ` R ) Y ) = Y )
28 27 27 oveq12d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) ( .r ` R ) Y ) .+ ( ( 1r ` R ) ( .r ` R ) Y ) ) = ( Y .+ Y ) )
29 25 28 eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) = ( Y .+ Y ) )
30 23 29 oveq12d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) X ) .+ ( ( ( 1r ` R ) .+ ( 1r ` R ) ) ( .r ` R ) Y ) ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
31 1 11 4 ringlidm 
 |-  ( ( R e. Ring /\ ( X .+ Y ) e. B ) -> ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) = ( X .+ Y ) )
32 3 14 31 syl2anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) = ( X .+ Y ) )
33 32 32 oveq12d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) .+ ( ( 1r ` R ) ( .r ` R ) ( X .+ Y ) ) ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
34 17 30 33 3eqtr3d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ ( Y .+ Y ) ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
35 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
36 3 35 syl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> R e. Grp )
37 1 2 ringacl 
 |-  ( ( R e. Ring /\ X e. B /\ X e. B ) -> ( X .+ X ) e. B )
38 3 9 9 37 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ X ) e. B )
39 1 2 grpass 
 |-  ( ( R e. Grp /\ ( ( X .+ X ) e. B /\ Y e. B /\ Y e. B ) ) -> ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
40 36 38 10 10 39 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
41 1 2 grpass 
 |-  ( ( R e. Grp /\ ( ( X .+ Y ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( X .+ Y ) .+ X ) .+ Y ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
42 36 14 9 10 41 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( X .+ Y ) .+ X ) .+ Y ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
43 34 40 42 3eqtr4d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( ( X .+ Y ) .+ X ) .+ Y ) )
44 1 2 ringacl 
 |-  ( ( R e. Ring /\ ( X .+ X ) e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) e. B )
45 3 38 10 44 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) e. B )
46 1 2 ringacl 
 |-  ( ( R e. Ring /\ ( X .+ Y ) e. B /\ X e. B ) -> ( ( X .+ Y ) .+ X ) e. B )
47 3 14 9 46 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .+ X ) e. B )
48 1 2 grprcan 
 |-  ( ( R e. Grp /\ ( ( ( X .+ X ) .+ Y ) e. B /\ ( ( X .+ Y ) .+ X ) e. B /\ Y e. B ) ) -> ( ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( ( X .+ Y ) .+ X ) .+ Y ) <-> ( ( X .+ X ) .+ Y ) = ( ( X .+ Y ) .+ X ) ) )
49 36 45 47 10 48 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( ( X .+ Y ) .+ X ) .+ Y ) <-> ( ( X .+ X ) .+ Y ) = ( ( X .+ Y ) .+ X ) ) )
50 43 49 mpbid 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) = ( ( X .+ Y ) .+ X ) )
51 1 2 grpass 
 |-  ( ( R e. Grp /\ ( X e. B /\ X e. B /\ Y e. B ) ) -> ( ( X .+ X ) .+ Y ) = ( X .+ ( X .+ Y ) ) )
52 36 9 9 10 51 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) = ( X .+ ( X .+ Y ) ) )
53 1 2 grpass 
 |-  ( ( R e. Grp /\ ( X e. B /\ Y e. B /\ X e. B ) ) -> ( ( X .+ Y ) .+ X ) = ( X .+ ( Y .+ X ) ) )
54 36 9 10 9 53 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .+ X ) = ( X .+ ( Y .+ X ) ) )
55 50 52 54 3eqtr3d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ ( X .+ Y ) ) = ( X .+ ( Y .+ X ) ) )
56 1 2 ringacl 
 |-  ( ( R e. Ring /\ Y e. B /\ X e. B ) -> ( Y .+ X ) e. B )
57 56 3com23 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( Y .+ X ) e. B )
58 1 2 grplcan 
 |-  ( ( R e. Grp /\ ( ( X .+ Y ) e. B /\ ( Y .+ X ) e. B /\ X e. B ) ) -> ( ( X .+ ( X .+ Y ) ) = ( X .+ ( Y .+ X ) ) <-> ( X .+ Y ) = ( Y .+ X ) ) )
59 36 14 57 9 58 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ ( X .+ Y ) ) = ( X .+ ( Y .+ X ) ) <-> ( X .+ Y ) = ( Y .+ X ) ) )
60 55 59 mpbid 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )