Theorem gsummptfzsplitl

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 AV, 7-Nov-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$$
	gsummptfzsplitl.y	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to Y\in B$$
Assertion	gsummptfzsplitl	$$⊢\phi \to \underset{k=0}{\overset{N}{{\sum }_G}}Y=\left(\underset{k=1}{\overset{N}{{\sum }_G}},Y\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{0\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		gsummptfzsplitl.y	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to Y\in B$$
6		fzfid	$$⊢\phi \to \left(0\dots N\right)\in \mathrm{Fin}$$
7		incom	$$⊢\left(1\dots N\right)\cap \left\{0\right\}=\left\{0\right\}\cap \left(1\dots N\right)$$
8	7	a1i	$$⊢\phi \to \left(1\dots N\right)\cap \left\{0\right\}=\left\{0\right\}\cap \left(1\dots N\right)$$
9		1e0p1	$$⊢1=0+1$$
10	9	oveq1i	$$⊢\left(1\dots N\right)=\left(0+1\dots N\right)$$
11	10	a1i	$$⊢\phi \to \left(1\dots N\right)=\left(0+1\dots N\right)$$
12	11	ineq2d	$$⊢\phi \to \left\{0\right\}\cap \left(1\dots N\right)=\left\{0\right\}\cap \left(0+1\dots N\right)$$
13		elnn0uz	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
14	13	biimpi	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{Z}}_{\ge 0}$$
15		fzpreddisj	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to \left\{0\right\}\cap \left(0+1\dots N\right)=\varnothing$$
16	4 14 15	3syl	$$⊢\phi \to \left\{0\right\}\cap \left(0+1\dots N\right)=\varnothing$$
17	8 12 16	3eqtrd	$$⊢\phi \to \left(1\dots N\right)\cap \left\{0\right\}=\varnothing$$
18		fzpred	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to \left(0\dots N\right)=\left\{0\right\}\cup \left(0+1\dots N\right)$$
19	4 14 18	3syl	$$⊢\phi \to \left(0\dots N\right)=\left\{0\right\}\cup \left(0+1\dots N\right)$$
20		uncom	$$⊢\left\{0\right\}\cup \left(0+1\dots N\right)=\left(0+1\dots N\right)\cup \left\{0\right\}$$
21		0p1e1	$$⊢0+1=1$$
22	21	oveq1i	$$⊢\left(0+1\dots N\right)=\left(1\dots N\right)$$
23	22	uneq1i	$$⊢\left(0+1\dots N\right)\cup \left\{0\right\}=\left(1\dots N\right)\cup \left\{0\right\}$$
24	20 23	eqtri	$$⊢\left\{0\right\}\cup \left(0+1\dots N\right)=\left(1\dots N\right)\cup \left\{0\right\}$$
25	19 24	syl6eq	$$⊢\phi \to \left(0\dots N\right)=\left(1\dots N\right)\cup \left\{0\right\}$$
26	1 2 3 6 5 17 25	gsummptfidmsplit	$$⊢\phi \to \underset{k=0}{\overset{N}{{\sum }_G}}Y=\left(\underset{k=1}{\overset{N}{{\sum }_G}},Y\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{0\right\}}{{\sum }_G},Y\right)$$