# 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}={\mathrm{Base}}_{{R}}$
ringacl.p
Assertion ringcom

### Proof

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