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 = ( Base ` G )
	nn0gsumfz.0	|- .0. = ( 0g ` G )
	nn0gsumfz.g	|- ( ph -> G e. CMnd )
	nn0gsumfz.f	|- ( ph -> F e. ( B ^m NN0 ) )
	nn0gsumfz.y	|- ( ph -> F finSupp .0. )
Assertion	nn0gsumfz0	|- ( ph -> E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( G gsum F ) = ( G gsum f ) )

Proof

Step	Hyp	Ref	Expression
1		nn0gsumfz.b	|- B = ( Base ` G )
2		nn0gsumfz.0	|- .0. = ( 0g ` G )
3		nn0gsumfz.g	|- ( ph -> G e. CMnd )
4		nn0gsumfz.f	|- ( ph -> F e. ( B ^m NN0 ) )
5		nn0gsumfz.y	|- ( ph -> F finSupp .0. )
6	1 2 3 4 5	nn0gsumfz	|- ( ph -> E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum f ) ) )
7		simp3	|- ( ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum f ) ) -> ( G gsum F ) = ( G gsum f ) )
8	7	reximi	|- ( E. f e. ( B ^m ( 0 ... s ) ) ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum f ) ) -> E. f e. ( B ^m ( 0 ... s ) ) ( G gsum F ) = ( G gsum f ) )
9	8	reximi	|- ( E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum f ) ) -> E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( G gsum F ) = ( G gsum f ) )
10	6 9	syl	|- ( ph -> E. s e. NN0 E. f e. ( B ^m ( 0 ... s ) ) ( G gsum F ) = ( G gsum f ) )