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	$⊢ \underset{˙}{+} = +_{R}$
Assertion	ringcom	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Proof

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

Metamath Proof Explorer

Theorem ringcom

Proof