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	$$⊢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$$
	gsummptfzsplitla.1	$$⊢\left(\phi \wedge k=M\right)\to Y=X$$
Assertion	gsummptfzsplitla	$$⊢\phi \to \underset{k=M}{\overset{N}{{\sum }_G}}Y=X\underset{\dot{}}{+}\left(\underset{k=M+1}{\overset{N}{{\sum }_G}},Y\right)$$

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		gsummptfzsplitla.1	$$⊢\left(\phi \wedge k=M\right)\to Y=X$$
7		fzfid	$$⊢\phi \to \left(M\dots N\right)\in \mathrm{Fin}$$
8		fzpreddisj	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left\{M\right\}\cap \left(M+1\dots N\right)=\varnothing$$
9	4 8	syl	$$⊢\phi \to \left\{M\right\}\cap \left(M+1\dots N\right)=\varnothing$$
10		fzpred	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)=\left\{M\right\}\cup \left(M+1\dots N\right)$$
11	4 10	syl	$$⊢\phi \to \left(M\dots N\right)=\left\{M\right\}\cup \left(M+1\dots 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\right\}}{{\sum }_G},Y\right)\underset{\dot{}}{+}\left(\underset{k=M+1}{\overset{N}{{\sum }_G}},Y\right)$$
13	3	cmnmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
14	4	elfvexd	$$⊢\phi \to M\in \mathrm{V}$$
15	14 6	csbied	$$⊢\phi \to ⦋M/k⦌Y=X$$
16		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
17	4 16	syl	$$⊢\phi \to M\in \left(M\dots N\right)$$
18	5	ralrimiva	$$⊢\phi \to \forall k\in \left(M\dots N\right)Y\in B$$
19		rspcsbela	$$⊢\left(M\in \left(M\dots N\right)\wedge \forall k\in \left(M\dots N\right)Y\in B\right)\to ⦋M/k⦌Y\in B$$
20	17 18 19	syl2anc	$$⊢\phi \to ⦋M/k⦌Y\in B$$
21	15 20	eqeltrrd	$$⊢\phi \to X\in B$$
22	1 13 14 21 6	gsumsnd	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }_G}Y=X$$
23	22	oveq1d	$$⊢\phi \to \left(\underset{k\in \left\{M\right\}}{{\sum }_G},Y\right)\underset{\dot{}}{+}\left(\underset{k=M+1}{\overset{N}{{\sum }_G}},Y\right)=X\underset{\dot{}}{+}\left(\underset{k=M+1}{\overset{N}{{\sum }_G}},Y\right)$$
24	12 23	eqtrd	$$⊢\phi \to \underset{k=M}{\overset{N}{{\sum }_G}}Y=X\underset{\dot{}}{+}\left(\underset{k=M+1}{\overset{N}{{\sum }_G}},Y\right)$$