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