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

Metamath Proof Explorer

Theorem gsummptfzsplitla

Description: Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the left. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummptfzsplita.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfzsplita.p ⊢ + = ( +g ‘ 𝐺 )
gsummptfzsplita.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptfzsplita.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
gsummptfzsplita.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
gsummptfzsplitla.1 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑌 = 𝑋 )
Assertion gsummptfzsplitla ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝑌 ) ) = ( 𝑋 + ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↦ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfzsplita.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfzsplita.p ⊢ + = ( +g ‘ 𝐺 )
3 gsummptfzsplita.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptfzsplita.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 gsummptfzsplita.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
6 gsummptfzsplitla.1 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑌 = 𝑋 )
7 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
8 fzpreddisj ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
9 4 8 syl ⊢ ( 𝜑 → ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
10 fzpred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
11 4 10 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
12 1 2 3 7 5 9 11 gsummptfidmsplit ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↦ 𝑌 ) ) ) )
13 3 cmnmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
14 4 elfvexd ⊢ ( 𝜑 → 𝑀 ∈ V )
15 14 6 csbied ⊢ ( 𝜑 → ⦋ 𝑀 / 𝑘 ⦌ 𝑌 = 𝑋 )
16 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
17 4 16 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
18 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑌 ∈ 𝐵 )
19 rspcsbela ⊢ ( ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑌 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝑌 ∈ 𝐵 )
20 17 18 19 syl2anc ⊢ ( 𝜑 → ⦋ 𝑀 / 𝑘 ⦌ 𝑌 ∈ 𝐵 )
21 15 20 eqeltrrd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
22 1 13 14 21 6 gsumsnd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑌 ) ) = 𝑋 )
23 22 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↦ 𝑌 ) ) ) = ( 𝑋 + ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↦ 𝑌 ) ) ) )
24 12 23 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝑌 ) ) = ( 𝑋 + ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↦ 𝑌 ) ) ) )