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={\mathrm{Base}}_R$$
	ringacl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	ringcom	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		ringacl.b	$$⊢B={\mathrm{Base}}_R$$
2		ringacl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3	1 2	ringcomlem	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Y\right)=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
4		simp1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to R\in \mathrm{Ring}$$
5	4	ringgrpd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to R\in \mathrm{Grp}$$
6		simp2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
7	1 2	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge X\in B\right)\to X\underset{\dot{}}{+}X\in B$$
8	4 6 6 7	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}X\in B$$
9		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
10	1 2	grpass	$$⊢\left(R\in \mathrm{Grp}\wedge \left(X\underset{\dot{}}{+}X\in B\wedge Y\in B\wedge Y\in B\right)\right)\to \left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Y\right)$$
11	5 8 9 9 10	syl13anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Y\right)$$
12	1 2	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
13	1 2	grpass	$$⊢\left(R\in \mathrm{Grp}\wedge \left(X\underset{\dot{}}{+}Y\in B\wedge X\in B\wedge Y\in B\right)\right)\to \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
14	5 12 6 9 13	syl13anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
15	3 11 14	3eqtr4d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Y=\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y$$
16	1 2	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge X\underset{\dot{}}{+}X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\in B$$
17	4 8 9 16	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\in B$$
18	1 2	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge X\underset{\dot{}}{+}Y\in B\wedge X\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\in B$$
19	4 12 6 18	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\in B$$
20	1 2	grprcan	$$⊢\left(R\in \mathrm{Grp}\wedge \left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\in B\wedge \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\in B\wedge Y\in B\right)\right)\to \left(\left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Y=\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\leftrightarrow \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)$$
21	5 17 19 9 20	syl13anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(\left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Y=\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\leftrightarrow \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X\right)$$
22	15 21	mpbid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
23	1 2	grpass	$$⊢\left(R\in \mathrm{Grp}\wedge \left(X\in B\wedge X\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
24	5 6 6 9 23	syl13anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
25	1 2	grpass	$$⊢\left(R\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\wedge X\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
26	5 6 9 6 25	syl13anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
27	22 24 26	3eqtr3d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
28	1 2	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to Y\underset{\dot{}}{+}X\in B$$
29	28	3com23	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to Y\underset{\dot{}}{+}X\in B$$
30	1 2	grplcan	$$⊢\left(R\in \mathrm{Grp}\wedge \left(X\underset{\dot{}}{+}Y\in B\wedge Y\underset{\dot{}}{+}X\in B\wedge X\in B\right)\right)\to \left(X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\leftrightarrow X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
31	5 12 29 6 30	syl13anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\leftrightarrow X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
32	27 31	mpbid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$