Theorem nn0gsumfz

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)$$
	nn0gsumfz.y	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	nn0gsumfz	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\exists f\in \left(B^{\left(0\dots s\right)}\right)\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\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		nn0gsumfz.y	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
6	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
7	4 6	jctir	$$⊢\phi \to \left(F\in \left(B^{{\mathbb{N}}_0}\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
8		fsuppmapnn0ub	$$⊢\left(F\in \left(B^{{\mathbb{N}}_0}\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(F\right)\to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
9	7 5 8	sylc	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)$$
10		eqidd	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to {F\upharpoonright }_{\left(0\dots s\right)}={F\upharpoonright }_{\left(0\dots s\right)}$$
11		simpr	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\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)$$
12	3	adantr	$$⊢\left(\phi \wedge s\in {\mathbb{N}}_0\right)\to G\in \mathrm{CMnd}$$
13	4	adantr	$$⊢\left(\phi \wedge s\in {\mathbb{N}}_0\right)\to F\in \left(B^{{\mathbb{N}}_0}\right)$$
14		simpr	$$⊢\left(\phi \wedge s\in {\mathbb{N}}_0\right)\to s\in {\mathbb{N}}_0$$
15		eqid	$$⊢{F\upharpoonright }_{\left(0\dots s\right)}={F\upharpoonright }_{\left(0\dots s\right)}$$
16	1 2 12 13 14 15	fsfnn0gsumfsffz	$$⊢\left(\phi \wedge s\in {\mathbb{N}}_0\right)\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\left({F\upharpoonright }_{\left(0\dots s\right)}\right)\right)$$
17	16	imp	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\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\left({F\upharpoonright }_{\left(0\dots s\right)}\right)$$
18	13	adantr	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\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)$$
19		fz0ssnn0	$$⊢\left(0\dots s\right)\subseteq {\mathbb{N}}_0$$
20		elmapssres	$$⊢\left(F\in \left(B^{{\mathbb{N}}_0}\right)\wedge \left(0\dots s\right)\subseteq {\mathbb{N}}_0\right)\to {F\upharpoonright }_{\left(0\dots s\right)}\in \left(B^{\left(0\dots s\right)}\right)$$
21	18 19 20	sylancl	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to {F\upharpoonright }_{\left(0\dots s\right)}\in \left(B^{\left(0\dots s\right)}\right)$$
22		eqeq1	$$⊢f={F\upharpoonright }_{\left(0\dots s\right)}\to \left(f={F\upharpoonright }_{\left(0\dots s\right)}\leftrightarrow {F\upharpoonright }_{\left(0\dots s\right)}={F\upharpoonright }_{\left(0\dots s\right)}\right)$$
23		oveq2	$$⊢f={F\upharpoonright }_{\left(0\dots s\right)}\to {\sum }_{G}f={\sum }_G\left({F\upharpoonright }_{\left(0\dots s\right)}\right)$$
24	23	eqeq2d	$$⊢f={F\upharpoonright }_{\left(0\dots s\right)}\to \left({\sum }_{G}F={\sum }_{G}f\leftrightarrow {\sum }_{G}F={\sum }_G\left({F\upharpoonright }_{\left(0\dots s\right)}\right)\right)$$
25	22 24	3anbi13d	$$⊢f={F\upharpoonright }_{\left(0\dots s\right)}\to \left(\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)\leftrightarrow \left({F\upharpoonright }_{\left(0\dots s\right)}={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_G\left({F\upharpoonright }_{\left(0\dots s\right)}\right)\right)\right)$$
26	25	adantl	$$⊢\left(\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\wedge f={F\upharpoonright }_{\left(0\dots s\right)}\right)\to \left(\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)\leftrightarrow \left({F\upharpoonright }_{\left(0\dots s\right)}={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_G\left({F\upharpoonright }_{\left(0\dots s\right)}\right)\right)\right)$$
27	21 26	rspcedv	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to \left(\left({F\upharpoonright }_{\left(0\dots s\right)}={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_G\left({F\upharpoonright }_{\left(0\dots s\right)}\right)\right)\to \exists f\in \left(B^{\left(0\dots s\right)}\right)\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)\right)$$
28	10 11 17 27	mp3and	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)\to \exists f\in \left(B^{\left(0\dots s\right)}\right)\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)$$
29	28	ex	$$⊢\left(\phi \wedge s\in {\mathbb{N}}_0\right)\to \left(\forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\to \exists f\in \left(B^{\left(0\dots s\right)}\right)\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)\right)$$
30	29	reximdva	$$⊢\phi \to \left(\exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\to \exists s\in {\mathbb{N}}_0\exists f\in \left(B^{\left(0\dots s\right)}\right)\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)\right)$$
31	9 30	mpd	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\exists f\in \left(B^{\left(0\dots s\right)}\right)\left(f={F\upharpoonright }_{\left(0\dots s\right)}\wedge \forall x\in {\mathbb{N}}_0\left(s<x\to F\left(x\right)=\underset{\dot{}}{0}\right)\wedge {\sum }_{G}F={\sum }_{G}f\right)$$