cmn246135

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

	Ref	Expression
Hypotheses	cmn135246.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cmn135246.2	⊢ + = ( +_g ‘ 𝐺 )
	cmn135246.3	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	cmn135246.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cmn135246.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	cmn135246.6	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	cmn135246.7	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	cmn135246.8	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
	cmn135246.9	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
Assertion	cmn246135	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) ) = ( ( 𝑌 + ( 𝑈 + 𝑊 ) ) + ( 𝑋 + ( 𝑍 + 𝑉 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cmn135246.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cmn135246.2	⊢ + = ( +_g ‘ 𝐺 )
3		cmn135246.3	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		cmn135246.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		cmn135246.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		cmn135246.6	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		cmn135246.7	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
8		cmn135246.8	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
9		cmn135246.9	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
10	1 2	cmncom	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
11	3 4 5 10	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
12	1 2 3 6 7 8 9	cmn4d	⊢ ( 𝜑 → ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) = ( ( 𝑍 + 𝑉 ) + ( 𝑈 + 𝑊 ) ) )
13	3	cmnmndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
14	1 2	mndcl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑍 + 𝑉 ) ∈ 𝐵 )
15	13 6 8 14	syl3anc	⊢ ( 𝜑 → ( 𝑍 + 𝑉 ) ∈ 𝐵 )
16	1 2	mndcl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑈 + 𝑊 ) ∈ 𝐵 )
17	13 7 9 16	syl3anc	⊢ ( 𝜑 → ( 𝑈 + 𝑊 ) ∈ 𝐵 )
18	1 2	cmncom	⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑍 + 𝑉 ) ∈ 𝐵 ∧ ( 𝑈 + 𝑊 ) ∈ 𝐵 ) → ( ( 𝑍 + 𝑉 ) + ( 𝑈 + 𝑊 ) ) = ( ( 𝑈 + 𝑊 ) + ( 𝑍 + 𝑉 ) ) )
19	3 15 17 18	syl3anc	⊢ ( 𝜑 → ( ( 𝑍 + 𝑉 ) + ( 𝑈 + 𝑊 ) ) = ( ( 𝑈 + 𝑊 ) + ( 𝑍 + 𝑉 ) ) )
20	12 19	eqtrd	⊢ ( 𝜑 → ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) = ( ( 𝑈 + 𝑊 ) + ( 𝑍 + 𝑉 ) ) )
21	11 20	oveq12d	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) ) = ( ( 𝑌 + 𝑋 ) + ( ( 𝑈 + 𝑊 ) + ( 𝑍 + 𝑉 ) ) ) )
22	1 2 3 5 4 17 15	cmn4d	⊢ ( 𝜑 → ( ( 𝑌 + 𝑋 ) + ( ( 𝑈 + 𝑊 ) + ( 𝑍 + 𝑉 ) ) ) = ( ( 𝑌 + ( 𝑈 + 𝑊 ) ) + ( 𝑋 + ( 𝑍 + 𝑉 ) ) ) )
23	21 22	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) ) = ( ( 𝑌 + ( 𝑈 + 𝑊 ) ) + ( 𝑋 + ( 𝑍 + 𝑉 ) ) ) )

Metamath Proof Explorer

Theorem cmn246135

Proof