This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmn145236

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

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 6 7 10 syl3anc ⊢ ( 𝜑 → ( 𝑍 + 𝑈 ) = ( 𝑈 + 𝑍 ) )
12 11 oveq1d ⊢ ( 𝜑 → ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) = ( ( 𝑈 + 𝑍 ) + ( 𝑉 + 𝑊 ) ) )
13 1 2 3 7 6 8 9 cmn4d ⊢ ( 𝜑 → ( ( 𝑈 + 𝑍 ) + ( 𝑉 + 𝑊 ) ) = ( ( 𝑈 + 𝑉 ) + ( 𝑍 + 𝑊 ) ) )
14 12 13 eqtrd ⊢ ( 𝜑 → ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) = ( ( 𝑈 + 𝑉 ) + ( 𝑍 + 𝑊 ) ) )
15 14 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) ) = ( ( 𝑋 + 𝑌 ) + ( ( 𝑈 + 𝑉 ) + ( 𝑍 + 𝑊 ) ) ) )
16 3 cmnmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
17 1 2 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑈 + 𝑉 ) ∈ 𝐵 )
18 16 7 8 17 syl3anc ⊢ ( 𝜑 → ( 𝑈 + 𝑉 ) ∈ 𝐵 )
19 1 2 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
20 16 6 9 19 syl3anc ⊢ ( 𝜑 → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
21 1 2 3 4 18 5 20 cmn4d ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑈 + 𝑉 ) ) + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) = ( ( 𝑋 + 𝑌 ) + ( ( 𝑈 + 𝑉 ) + ( 𝑍 + 𝑊 ) ) ) )
22 15 21 eqtr4d ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( ( 𝑍 + 𝑈 ) + ( 𝑉 + 𝑊 ) ) ) = ( ( 𝑋 + ( 𝑈 + 𝑉 ) ) + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) )