Theorem gsummptfzsplit

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 AV, 25-Oct-2019)

	Ref	Expression
Hypotheses	gsummptfzsplit.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptfzsplit.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsummptfzsplit.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptfzsplit.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	gsummptfzsplit.y	$$⊢\left(\phi \wedge k\in \left(0\dots N+1\right)\right)\to Y\in B$$
Assertion	gsummptfzsplit	$$⊢\phi \to \underset{k=0}{\overset{N+1}{{\sum }_G}}Y=\left(\underset{k=0}{\overset{N}{{\sum }_G}},Y\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{N+1\right\}}{{\sum }_G},Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptfzsplit.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfzsplit.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsummptfzsplit.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptfzsplit.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		gsummptfzsplit.y	$$⊢\left(\phi \wedge k\in \left(0\dots N+1\right)\right)\to Y\in B$$
6		fzfid	$$⊢\phi \to \left(0\dots N+1\right)\in \mathrm{Fin}$$
7		fzp1disj	$$⊢\left(0\dots N\right)\cap \left\{N+1\right\}=\varnothing$$
8	7	a1i	$$⊢\phi \to \left(0\dots N\right)\cap \left\{N+1\right\}=\varnothing$$
9		elnn0uz	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
10	4 9	sylib	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 0}$$
11		fzsuc	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to \left(0\dots N+1\right)=\left(0\dots N\right)\cup \left\{N+1\right\}$$
12	10 11	syl	$$⊢\phi \to \left(0\dots N+1\right)=\left(0\dots N\right)\cup \left\{N+1\right\}$$
13	1 2 3 6 5 8 12	gsummptfidmsplit	$$⊢\phi \to \underset{k=0}{\overset{N+1}{{\sum }_G}}Y=\left(\underset{k=0}{\overset{N}{{\sum }_G}},Y\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{N+1\right\}}{{\sum }_G},Y\right)$$