cmn145236

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	cmn145236	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} ((Z \underset{˙}{+} U) \underset{˙}{+} (V \underset{˙}{+} W)) = (X \underset{˙}{+} (U \underset{˙}{+} V)) \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W))$

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 Z \in B \land U \in B) \to Z \underset{˙}{+} U = U \underset{˙}{+} Z$
11	3 6 7 10	syl3anc	$⊢ φ \to Z \underset{˙}{+} U = U \underset{˙}{+} Z$
12	11	oveq1d	$⊢ φ \to (Z \underset{˙}{+} U) \underset{˙}{+} (V \underset{˙}{+} W) = (U \underset{˙}{+} Z) \underset{˙}{+} (V \underset{˙}{+} W)$
13	1 2 3 7 6 8 9	cmn4d	$⊢ φ \to (U \underset{˙}{+} Z) \underset{˙}{+} (V \underset{˙}{+} W) = (U \underset{˙}{+} V) \underset{˙}{+} (Z \underset{˙}{+} W)$
14	12 13	eqtrd	$⊢ φ \to (Z \underset{˙}{+} U) \underset{˙}{+} (V \underset{˙}{+} W) = (U \underset{˙}{+} V) \underset{˙}{+} (Z \underset{˙}{+} W)$
15	14	oveq2d	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} ((Z \underset{˙}{+} U) \underset{˙}{+} (V \underset{˙}{+} W)) = (X \underset{˙}{+} Y) \underset{˙}{+} ((U \underset{˙}{+} V) \underset{˙}{+} (Z \underset{˙}{+} W))$
16	3	cmnmndd	$⊢ φ \to G \in Mnd$
17	1 2	mndcl	$⊢ (G \in Mnd \land U \in B \land V \in B) \to U \underset{˙}{+} V \in B$
18	16 7 8 17	syl3anc	$⊢ φ \to U \underset{˙}{+} V \in B$
19	1 2	mndcl	$⊢ (G \in Mnd \land Z \in B \land W \in B) \to Z \underset{˙}{+} W \in B$
20	16 6 9 19	syl3anc	$⊢ φ \to Z \underset{˙}{+} W \in B$
21	1 2 3 4 18 5 20	cmn4d	$⊢ φ \to (X \underset{˙}{+} (U \underset{˙}{+} V)) \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W)) = (X \underset{˙}{+} Y) \underset{˙}{+} ((U \underset{˙}{+} V) \underset{˙}{+} (Z \underset{˙}{+} W))$
22	15 21	eqtr4d	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} ((Z \underset{˙}{+} U) \underset{˙}{+} (V \underset{˙}{+} W)) = (X \underset{˙}{+} (U \underset{˙}{+} V)) \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W))$

Metamath Proof Explorer

Theorem cmn145236

Proof