Theorem fsfnn0gsumfsffz

Description: Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019)

	Ref	Expression
Hypotheses	nn0gsumfz.b	$$⊢B={\mathrm{Base}}_G$$
	nn0gsumfz.0	$$⊢\underset{\dot{}}{0}=0_G$$
	nn0gsumfz.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	nn0gsumfz.f	$$⊢\phi \to F\in \left(B^{{\mathbb{N}}_0}\right)$$
	fsfnn0gsumfsffz.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	fsfnn0gsumfsffz.h	$$⊢H={F\upharpoonright }_{\left(0\dots S\right)}$$
Assertion	fsfnn0gsumfsffz	$$⊢\phi \to \left(\forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\to {\sum }_{G}F={\sum }_{G}H\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0gsumfz.b	$$⊢B={\mathrm{Base}}_G$$
2		nn0gsumfz.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		nn0gsumfz.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		nn0gsumfz.f	$$⊢\phi \to F\in \left(B^{{\mathbb{N}}_0}\right)$$
5		fsfnn0gsumfsffz.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
6		fsfnn0gsumfsffz.h	$$⊢H={F\upharpoonright }_{\left(0\dots S\right)}$$
7	6	oveq2i	$$⊢{\sum }_{G}H={\sum }_G\left({F\upharpoonright }_{\left(0\dots S\right)}\right)$$
8	3	adantr	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to G\in \mathrm{CMnd}$$
9		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
10	9	a1i	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
11		elmapi	$$⊢F\in \left(B^{{\mathbb{N}}_0}\right)\to F:{\mathbb{N}}_0⟶B$$
12	4 11	syl	$$⊢\phi \to F:{\mathbb{N}}_0⟶B$$
13	12	adantr	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to F:{\mathbb{N}}_0⟶B$$
14	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
15	14	a1i	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
16	4	adantr	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to F\in \left(B^{{\mathbb{N}}_0}\right)$$
17	5	adantr	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to S\in {\mathbb{N}}_0$$
18		simpr	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)$$
19	15 16 17 18	suppssfz	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left(0\dots S\right)$$
20		elmapfun	$$⊢F\in \left(B^{{\mathbb{N}}_0}\right)\to \mathrm{Fun}F$$
21	4 20	syl	$$⊢\phi \to \mathrm{Fun}F$$
22	14	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
23	4 21 22	3jca	$$⊢\phi \to \left(F\in \left(B^{{\mathbb{N}}_0}\right)\wedge \mathrm{Fun}F\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
24		fzfid	$$⊢\phi \to \left(0\dots S\right)\in \mathrm{Fin}$$
25	24	anim1i	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left(0\dots S\right)\right)\to \left(\left(0\dots S\right)\in \mathrm{Fin}\wedge F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left(0\dots S\right)\right)$$
26		suppssfifsupp	$$⊢\left(\left(F\in \left(B^{{\mathbb{N}}_0}\right)\wedge \mathrm{Fun}F\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\wedge \left(\left(0\dots S\right)\in \mathrm{Fin}\wedge F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left(0\dots S\right)\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
27	23 25 26	syl2an2r	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left(0\dots S\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
28	19 27	syldan	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
29	1 2 8 10 13 19 28	gsumres	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to {\sum }_G\left({F\upharpoonright }_{\left(0\dots S\right)}\right)={\sum }_{G}F$$
30	7 29	syl5req	$$⊢\left(\phi \wedge \forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to {\sum }_{G}F={\sum }_{G}H$$
31	30	ex	$$⊢\phi \to \left(\forall x\in {\mathbb{N}}_0\left(S<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\to {\sum }_{G}F={\sum }_{G}H\right)$$