Theorem gsummptnn0fzfv

Description: A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019)

	Ref	Expression
Hypotheses	gsummptnn0fzfv.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptnn0fzfv.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummptnn0fzfv.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptnn0fzfv.f	$$⊢\phi \to F\in \left(B^{{\mathbb{N}}_0}\right)$$
	gsummptnn0fzfv.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	gsummptnn0fzfv.u	$$⊢\phi \to \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)$$
Assertion	gsummptnn0fzfv	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_G}F\left(k\right)=\underset{k=0}{\overset{S}{{\sum }_G}}F\left(k\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptnn0fzfv.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptnn0fzfv.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummptnn0fzfv.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptnn0fzfv.f	$$⊢\phi \to F\in \left(B^{{\mathbb{N}}_0}\right)$$
5		gsummptnn0fzfv.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
6		gsummptnn0fzfv.u	$$⊢\phi \to \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)$$
7		elmapi	$$⊢F\in \left(B^{{\mathbb{N}}_0}\right)\to F:{\mathbb{N}}_0⟶B$$
8		ffvelrn	$$⊢\left(F:{\mathbb{N}}_0⟶B\wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)\in B$$
9	8	ex	$$⊢F:{\mathbb{N}}_0⟶B\to \left(k\in {\mathbb{N}}_0\to F\left(k\right)\in B\right)$$
10	4 7 9	3syl	$$⊢\phi \to \left(k\in {\mathbb{N}}_0\to F\left(k\right)\in B\right)$$
11	10	ralrimiv	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}F\left(k\right)\in B$$
12		breq2	$$⊢x=k\to \left(S<x\leftrightarrow S<k\right)$$
13		fveqeq2	$$⊢x=k\to \left(F\left(x\right)=\underset{\dot{}}{0}\leftrightarrow F\left(k\right)=\underset{\dot{}}{0}\right)$$
14	12 13	imbi12d	$$⊢x=k\to \left(\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<k\to F\left(k\right)=\underset{\dot{}}{0}\right)\right)$$
15	14	cbvralvw	$$⊢\forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\leftrightarrow \forall k\in {\mathbb{N}}_0\left(S<k\to F\left(k\right)=\underset{\dot{}}{0}\right)$$
16	6 15	sylib	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(S<k\to F\left(k\right)=\underset{\dot{}}{0}\right)$$
17	1 2 3 11 5 16	gsummptnn0fz	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_G}F\left(k\right)=\underset{k=0}{\overset{S}{{\sum }_G}}F\left(k\right)$$