Theorem cmn246135

Description: Rearrange terms in a commutative monoid sum. Lemma for rlocaddval . (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	cmn135246.1	$$⊢B={\mathrm{Base}}_G$$
	cmn135246.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	cmn135246.3	$$⊢\phi \to G\in \mathrm{CMnd}$$
	cmn135246.5	$$⊢\phi \to X\in B$$
	cmn135246.4	$$⊢\phi \to Y\in B$$
	cmn135246.6	$$⊢\phi \to Z\in B$$
	cmn135246.7	$$⊢\phi \to U\in B$$
	cmn135246.8	$$⊢\phi \to V\in B$$
	cmn135246.9	$$⊢\phi \to W\in B$$
Assertion	cmn246135	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(\left(Z\underset{\dot{}}{+}U\right)\underset{\dot{}}{+}\left(V\underset{\dot{}}{+}W\right)\right)=\left(Y\underset{\dot{}}{+}\left(U\underset{\dot{}}{+}W\right)\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cmn135246.1	$$⊢B={\mathrm{Base}}_G$$
2		cmn135246.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		cmn135246.3	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		cmn135246.5	$$⊢\phi \to X\in B$$
5		cmn135246.4	$$⊢\phi \to Y\in B$$
6		cmn135246.6	$$⊢\phi \to Z\in B$$
7		cmn135246.7	$$⊢\phi \to U\in B$$
8		cmn135246.8	$$⊢\phi \to V\in B$$
9		cmn135246.9	$$⊢\phi \to W\in B$$
10	1 2	cmncom	$$⊢\left(G\in \mathrm{CMnd}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
11	3 4 5 10	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
12	1 2 3 6 7 8 9	cmn4d	$$⊢\phi \to \left(Z\underset{\dot{}}{+}U\right)\underset{\dot{}}{+}\left(V\underset{\dot{}}{+}W\right)=\left(Z\underset{\dot{}}{+}V\right)\underset{\dot{}}{+}\left(U\underset{\dot{}}{+}W\right)$$
13	3	cmnmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
14	1 2	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge Z\in B\wedge V\in B\right)\to Z\underset{\dot{}}{+}V\in B$$
15	13 6 8 14	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{+}V\in B$$
16	1 2	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge U\in B\wedge W\in B\right)\to U\underset{\dot{}}{+}W\in B$$
17	13 7 9 16	syl3anc	$$⊢\phi \to U\underset{\dot{}}{+}W\in B$$
18	1 2	cmncom	$$⊢\left(G\in \mathrm{CMnd}\wedge Z\underset{\dot{}}{+}V\in B\wedge U\underset{\dot{}}{+}W\in B\right)\to \left(Z\underset{\dot{}}{+}V\right)\underset{\dot{}}{+}\left(U\underset{\dot{}}{+}W\right)=\left(U\underset{\dot{}}{+}W\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)$$
19	3 15 17 18	syl3anc	$$⊢\phi \to \left(Z\underset{\dot{}}{+}V\right)\underset{\dot{}}{+}\left(U\underset{\dot{}}{+}W\right)=\left(U\underset{\dot{}}{+}W\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)$$
20	12 19	eqtrd	$$⊢\phi \to \left(Z\underset{\dot{}}{+}U\right)\underset{\dot{}}{+}\left(V\underset{\dot{}}{+}W\right)=\left(U\underset{\dot{}}{+}W\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)$$
21	11 20	oveq12d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(\left(Z\underset{\dot{}}{+}U\right)\underset{\dot{}}{+}\left(V\underset{\dot{}}{+}W\right)\right)=\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(\left(U\underset{\dot{}}{+}W\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)\right)$$
22	1 2 3 5 4 17 15	cmn4d	$$⊢\phi \to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(\left(U\underset{\dot{}}{+}W\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)\right)=\left(Y\underset{\dot{}}{+}\left(U\underset{\dot{}}{+}W\right)\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)\right)$$
23	21 22	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(\left(Z\underset{\dot{}}{+}U\right)\underset{\dot{}}{+}\left(V\underset{\dot{}}{+}W\right)\right)=\left(Y\underset{\dot{}}{+}\left(U\underset{\dot{}}{+}W\right)\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}V\right)\right)$$