Theorem gsummptnn0fz

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

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

Proof

Step	Hyp	Ref	Expression
1		gsummptnn0fz.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptnn0fz.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummptnn0fz.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptnn0fz.f	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}C\in B$$
5		gsummptnn0fz.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
6		gsummptnn0fz.u	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)$$
7		nfv	$$⊢Ⅎx\left(S<k\to C=\underset{\dot{}}{0}\right)$$
8		nfv	$$⊢ℲkS<x$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋x/k⦌C$$
10	9	nfeq1	$$⊢Ⅎk⦋x/k⦌C=\underset{\dot{}}{0}$$
11	8 10	nfim	$$⊢Ⅎk\left(S<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
12		breq2	$$⊢k=x\to \left(S<k\leftrightarrow S<x\right)$$
13		csbeq1a	$$⊢k=x\to C=⦋x/k⦌C$$
14	13	eqeq1d	$$⊢k=x\to \left(C=\underset{\dot{}}{0}\leftrightarrow ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
15	12 14	imbi12d	$$⊢k=x\to \left(\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)\right)$$
16	7 11 15	cbvralw	$$⊢\forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(S<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
17	6 16	sylib	$$⊢\phi \to \forall x\in {\mathbb{N}}_0\left(S<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
18		simpr	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to x\in {\mathbb{N}}_0$$
19	4	anim1ci	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(x\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)$$
20		rspcsbela	$$⊢\left(x\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)\to ⦋x/k⦌C\in B$$
21	19 20	syl	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to ⦋x/k⦌C\in B$$
22	18 21	jca	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(x\in {\mathbb{N}}_0\wedge ⦋x/k⦌C\in B\right)$$
23	22	adantr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge ⦋x/k⦌C=\underset{\dot{}}{0}\right)\to \left(x\in {\mathbb{N}}_0\wedge ⦋x/k⦌C\in B\right)$$
24		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼C\right)=\left(k\in {\mathbb{N}}_0⟼C\right)$$
25	24	fvmpts	$$⊢\left(x\in {\mathbb{N}}_0\wedge ⦋x/k⦌C\in B\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=⦋x/k⦌C$$
26	23 25	syl	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge ⦋x/k⦌C=\underset{\dot{}}{0}\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=⦋x/k⦌C$$
27		simpr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge ⦋x/k⦌C=\underset{\dot{}}{0}\right)\to ⦋x/k⦌C=\underset{\dot{}}{0}$$
28	26 27	eqtrd	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge ⦋x/k⦌C=\underset{\dot{}}{0}\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}$$
29	28	ex	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(⦋x/k⦌C=\underset{\dot{}}{0}\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
30	29	imim2d	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(\left(S<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)\to \left(S<x\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
31	30	ralimdva	$$⊢\phi \to \left(\forall x\in {\mathbb{N}}_0\left(S<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)\to \forall x\in {\mathbb{N}}_0\left(S<x\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
32	17 31	mpd	$$⊢\phi \to \forall x\in {\mathbb{N}}_0\left(S<x\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
33	24	fmpt	$$⊢\forall k\in {\mathbb{N}}_{0}C\in B\leftrightarrow \left(k\in {\mathbb{N}}_0⟼C\right):{\mathbb{N}}_0⟶B$$
34	4 33	sylib	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼C\right):{\mathbb{N}}_0⟶B$$
35	1	fvexi	$$⊢B\in \mathrm{V}$$
36		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
37	35 36	pm3.2i	$$⊢\left(B\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)$$
38		elmapg	$$⊢\left(B\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\in \left(B^{{\mathbb{N}}_0}\right)\leftrightarrow \left(k\in {\mathbb{N}}_0⟼C\right):{\mathbb{N}}_0⟶B\right)$$
39	37 38	mp1i	$$⊢\phi \to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\in \left(B^{{\mathbb{N}}_0}\right)\leftrightarrow \left(k\in {\mathbb{N}}_0⟼C\right):{\mathbb{N}}_0⟶B\right)$$
40	34 39	mpbird	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼C\right)\in \left(B^{{\mathbb{N}}_0}\right)$$
41		fz0ssnn0	$$⊢\left(0\dots S\right)\subseteq {\mathbb{N}}_0$$
42		resmpt	$$⊢\left(0\dots S\right)\subseteq {\mathbb{N}}_0\to {\left(k\in {\mathbb{N}}_0⟼C\right)\upharpoonright }_{\left(0\dots S\right)}=\left(k\in \left(0\dots S\right)⟼C\right)$$
43	41 42	ax-mp	$$⊢{\left(k\in {\mathbb{N}}_0⟼C\right)\upharpoonright }_{\left(0\dots S\right)}=\left(k\in \left(0\dots S\right)⟼C\right)$$
44	43	eqcomi	$$⊢\left(k\in \left(0\dots S\right)⟼C\right)={\left(k\in {\mathbb{N}}_0⟼C\right)\upharpoonright }_{\left(0\dots S\right)}$$
45	1 2 3 40 5 44	fsfnn0gsumfsffz	$$⊢\phi \to \left(\forall x\in {\mathbb{N}}_0\left(S<x\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_G}C=\underset{k=0}{\overset{S}{{\sum }_G}}C\right)$$
46	32 45	mpd	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_G}C=\underset{k=0}{\overset{S}{{\sum }_G}}C$$