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 = {Base}_{G}$
	cmn135246.2	$⊢ \underset{˙}{+} = +_{G}$
	cmn135246.3	$⊢ φ \to G \in CMnd$
	cmn135246.5	$⊢ φ \to X \in B$
	cmn135246.4	$⊢ φ \to Y \in B$
	cmn135246.6	$⊢ φ \to Z \in B$
	cmn135246.7	$⊢ φ \to U \in B$
	cmn135246.8	$⊢ φ \to V \in B$
	cmn135246.9	$⊢ φ \to W \in B$
Assertion	cmn246135	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} ((Z \underset{˙}{+} U) \underset{˙}{+} (V \underset{˙}{+} W)) = (Y \underset{˙}{+} (U \underset{˙}{+} W)) \underset{˙}{+} (X \underset{˙}{+} (Z \underset{˙}{+} V))$

Proof

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

Metamath Proof Explorer

Theorem cmn246135

Proof