Theorem gsummptfzsplitra

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 right. (Contributed by Thierry Arnoux, 15-Feb-2026)

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

Proof

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