Metamath Proof Explorer

Theorem ringcom

Description: Commutativity of the additive group of a ring. (See also lmodcom .) This proof requires the existence of a multiplicative identity, and the existence of additive inverses. Therefore, this proof is not applicable for semirings. (Contributed by Gérard Lang, 4-Dec-2014) (Proof shortened by AV, 1-Feb-2025)

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 1 2 ringcomlem 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ ( Y .+ Y ) ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
4 simp1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> R e. Ring )
5 4 ringgrpd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> R e. Grp )
6 simp2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> X e. B )
7 1 2 ringacl 
 |-  ( ( R e. Ring /\ X e. B /\ X e. B ) -> ( X .+ X ) e. B )
8 4 6 6 7 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ X ) e. B )
9 simp3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> Y e. B )
10 1 2 grpass 
 |-  ( ( R e. Grp /\ ( ( X .+ X ) e. B /\ Y e. B /\ Y e. B ) ) -> ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
11 5 8 9 9 10 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
12 1 2 ringacl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
13 1 2 grpass 
 |-  ( ( R e. Grp /\ ( ( X .+ Y ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( X .+ Y ) .+ X ) .+ Y ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
14 5 12 6 9 13 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( X .+ Y ) .+ X ) .+ Y ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
15 3 11 14 3eqtr4d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( ( X .+ Y ) .+ X ) .+ Y ) )
16 1 2 ringacl 
 |-  ( ( R e. Ring /\ ( X .+ X ) e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) e. B )
17 4 8 9 16 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) e. B )
18 1 2 ringacl 
 |-  ( ( R e. Ring /\ ( X .+ Y ) e. B /\ X e. B ) -> ( ( X .+ Y ) .+ X ) e. B )
19 4 12 6 18 syl3anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .+ X ) e. B )
20 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 ) ) )
21 5 17 19 9 20 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( ( ( X .+ X ) .+ Y ) .+ Y ) = ( ( ( X .+ Y ) .+ X ) .+ Y ) <-> ( ( X .+ X ) .+ Y ) = ( ( X .+ Y ) .+ X ) ) )
22 15 21 mpbid 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) = ( ( X .+ Y ) .+ X ) )
23 1 2 grpass 
 |-  ( ( R e. Grp /\ ( X e. B /\ X e. B /\ Y e. B ) ) -> ( ( X .+ X ) .+ Y ) = ( X .+ ( X .+ Y ) ) )
24 5 6 6 9 23 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ X ) .+ Y ) = ( X .+ ( X .+ Y ) ) )
25 1 2 grpass 
 |-  ( ( R e. Grp /\ ( X e. B /\ Y e. B /\ X e. B ) ) -> ( ( X .+ Y ) .+ X ) = ( X .+ ( Y .+ X ) ) )
26 5 6 9 6 25 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .+ X ) = ( X .+ ( Y .+ X ) ) )
27 22 24 26 3eqtr3d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ ( X .+ Y ) ) = ( X .+ ( Y .+ X ) ) )
28 1 2 ringacl 
 |-  ( ( R e. Ring /\ Y e. B /\ X e. B ) -> ( Y .+ X ) e. B )
29 28 3com23 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( Y .+ X ) e. B )
30 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 ) ) )
31 5 12 29 6 30 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( ( X .+ ( X .+ Y ) ) = ( X .+ ( Y .+ X ) ) <-> ( X .+ Y ) = ( Y .+ X ) ) )
32 27 31 mpbid 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )