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	$$⊢B={\mathrm{Base}}_G$$
	gsummptfzsplita.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsummptfzsplita.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptfzsplita.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	gsummptfzsplita.y	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to Y\in B$$
	gsummptfzsplitra.1	$$⊢\left(\phi \wedge k=N\right)\to Y=X$$
Assertion	gsummptfzsplitra	$$⊢\phi \to \underset{k=M}{\overset{N}{{\sum }_G}}Y=\left(\underset{k\in \left(M..^N\right)}{{\sum }_G},Y\right)\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		gsummptfzsplita.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfzsplita.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsummptfzsplita.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptfzsplita.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
5		gsummptfzsplita.y	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to Y\in B$$
6		gsummptfzsplitra.1	$$⊢\left(\phi \wedge k=N\right)\to Y=X$$
7		fzfid	$$⊢\phi \to \left(M\dots N\right)\in \mathrm{Fin}$$
8		fzodisjsn	$$⊢\left(M..^N\right)\cap \left\{N\right\}=\varnothing$$
9	8	a1i	$$⊢\phi \to \left(M..^N\right)\cap \left\{N\right\}=\varnothing$$
10		fzisfzounsn	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)=\left(M..^N\right)\cup \left\{N\right\}$$
11	4 10	syl	$$⊢\phi \to \left(M\dots N\right)=\left(M..^N\right)\cup \left\{N\right\}$$
12	1 2 3 7 5 9 11	gsummptfidmsplit	$$⊢\phi \to \underset{k=M}{\overset{N}{{\sum }_G}}Y=\left(\underset{k\in \left(M..^N\right)}{{\sum }_G},Y\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{N\right\}}{{\sum }_G},Y\right)$$
13	3	cmnmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
14	4 6	csbied	$$⊢\phi \to ⦋N/k⦌Y=X$$
15		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$
16	4 15	syl	$$⊢\phi \to N\in \left(M\dots N\right)$$
17	5	ralrimiva	$$⊢\phi \to \forall k\in \left(M\dots N\right)Y\in B$$
18		rspcsbela	$$⊢\left(N\in \left(M\dots N\right)\wedge \forall k\in \left(M\dots N\right)Y\in B\right)\to ⦋N/k⦌Y\in B$$
19	16 17 18	syl2anc	$$⊢\phi \to ⦋N/k⦌Y\in B$$
20	14 19	eqeltrrd	$$⊢\phi \to X\in B$$
21	1 13 4 20 6	gsumsnd	$$⊢\phi \to \underset{k\in \left\{N\right\}}{{\sum }_G}Y=X$$
22	21	oveq2d	$$⊢\phi \to \left(\underset{k\in \left(M..^N\right)}{{\sum }_G},Y\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{N\right\}}{{\sum }_G},Y\right)=\left(\underset{k\in \left(M..^N\right)}{{\sum }_G},Y\right)\underset{\dot{}}{+}X$$
23	12 22	eqtrd	$$⊢\phi \to \underset{k=M}{\overset{N}{{\sum }_G}}Y=\left(\underset{k\in \left(M..^N\right)}{{\sum }_G},Y\right)\underset{\dot{}}{+}X$$