Theorem nn0gsumfz0

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	nn0gsumfz0	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\exists f\in \left(B^{\left(0\dots s\right)}\right){\sum }_{G}F={\sum }_{G}f$$

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	1 2 3 4 5	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)$$
7		simp3	$$⊢\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)\to {\sum }_{G}F={\sum }_{G}f$$
8	7	reximi	$$⊢\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)\to \exists f\in \left(B^{\left(0\dots s\right)}\right){\sum }_{G}F={\sum }_{G}f$$
9	8	reximi	$$⊢\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)\to \exists s\in {\mathbb{N}}_0\exists f\in \left(B^{\left(0\dots s\right)}\right){\sum }_{G}F={\sum }_{G}f$$
10	6 9	syl	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\exists f\in \left(B^{\left(0\dots s\right)}\right){\sum }_{G}F={\sum }_{G}f$$