Theorem srgcom4

Description: Restricted commutativity of the addition in semirings (without using the commutativity of the addition given per definition of a semiring). (Contributed by AV, 1-Feb-2025) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	srgcom4.b	$$⊢B={\mathrm{Base}}_R$$
	srgcom4.p	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	srgcom4	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		srgcom4.b	$$⊢B={\mathrm{Base}}_R$$
2		srgcom4.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		srgmnd	$$⊢R\in \mathrm{SRing}\to R\in \mathrm{Mnd}$$
4	3	3ad2ant1	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to R\in \mathrm{Mnd}$$
5		simp2	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
6		simp3	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
7	1 2	mndass	$$⊢\left(R\in \mathrm{Mnd}\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)$$
8	4 5 5 6 7	syl13anc	$$⊢\left(R\in \mathrm{SRing}\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)$$
9	8	eqcomd	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y$$
10	9	oveq1d	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}Y=\left(\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Y$$
11	1 2	srgacl	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge X\in B\right)\to X\underset{\dot{}}{+}X\in B$$
12	5 11	syld3an3	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}X\in B$$
13	1 2	mndass	$$⊢\left(R\in \mathrm{Mnd}\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)$$
14	4 12 6 6 13	syl13anc	$$⊢\left(R\in \mathrm{SRing}\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)$$
15	1 2	srgcom4lem	$$⊢\left(R\in \mathrm{SRing}\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)$$
16	1 2	srgacl	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
17	1 2	mndass	$$⊢\left(R\in \mathrm{Mnd}\wedge \left(X\in B\wedge Y\in B\wedge X\underset{\dot{}}{+}Y\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)$$
18	4 5 6 16 17	syl13anc	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)$$
19	1 2	mndass	$$⊢\left(R\in \mathrm{Mnd}\wedge \left(Y\in B\wedge X\in B\wedge Y\in B\right)\right)\to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
20	19	eqcomd	$$⊢\left(R\in \mathrm{Mnd}\wedge \left(Y\in B\wedge X\in B\wedge Y\in B\right)\right)\to Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y$$
21	4 6 5 6 20	syl13anc	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y$$
22	21	oveq2d	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)=X\underset{\dot{}}{+}\left(\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)$$
23	1 2	srgacl	$$⊢\left(R\in \mathrm{SRing}\wedge Y\in B\wedge X\in B\right)\to Y\underset{\dot{}}{+}X\in B$$
24	23	3com23	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to Y\underset{\dot{}}{+}X\in B$$
25	1 2	mndass	$$⊢\left(R\in \mathrm{Mnd}\wedge \left(X\in B\wedge Y\underset{\dot{}}{+}X\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)$$
26	25	eqcomd	$$⊢\left(R\in \mathrm{Mnd}\wedge \left(X\in B\wedge Y\underset{\dot{}}{+}X\in B\wedge Y\in B\right)\right)\to X\underset{\dot{}}{+}\left(\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)=\left(X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y$$
27	4 5 24 6 26	syl13anc	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}\left(\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\right)=\left(X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y$$
28	22 27	eqtrd	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)=\left(X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y$$
29	15 18 28	3eqtrd	$$⊢\left(R\in \mathrm{SRing}\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{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y$$
30	10 14 29	3eqtrd	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}Y=\left(X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{+}Y$$