Metamath Proof Explorer

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 ⊢ 𝐵 = ( 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 ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) ) = ( ( 𝑌 + ( 𝑈 + 𝑊 ) ) + ( 𝑋 + ( 𝑍 + 𝑉 ) ) ) )