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 ) ... 𝑁 ) ↦ 𝑌 ) ) ) )