Theorem gsummptnn0fzfv

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

	Ref	Expression
Hypotheses	gsummptnn0fzfv.b	|- B = ( Base ` G )
	gsummptnn0fzfv.0	|- .0. = ( 0g ` G )
	gsummptnn0fzfv.g	|- ( ph -> G e. CMnd )
	gsummptnn0fzfv.f	|- ( ph -> F e. ( B ^m NN0 ) )
	gsummptnn0fzfv.s	|- ( ph -> S e. NN0 )
	gsummptnn0fzfv.u	|- ( ph -> A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) )
Assertion	gsummptnn0fzfv	|- ( ph -> ( G gsum ( k e. NN0 |-> ( F ` k ) ) ) = ( G gsum ( k e. ( 0 ... S ) |-> ( F ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptnn0fzfv.b	|- B = ( Base ` G )
2		gsummptnn0fzfv.0	|- .0. = ( 0g ` G )
3		gsummptnn0fzfv.g	|- ( ph -> G e. CMnd )
4		gsummptnn0fzfv.f	|- ( ph -> F e. ( B ^m NN0 ) )
5		gsummptnn0fzfv.s	|- ( ph -> S e. NN0 )
6		gsummptnn0fzfv.u	|- ( ph -> A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) )
7		elmapi	|- ( F e. ( B ^m NN0 ) -> F : NN0 --> B )
8		ffvelrn	|- ( ( F : NN0 --> B /\ k e. NN0 ) -> ( F ` k ) e. B )
9	8	ex	|- ( F : NN0 --> B -> ( k e. NN0 -> ( F ` k ) e. B ) )
10	4 7 9	3syl	|- ( ph -> ( k e. NN0 -> ( F ` k ) e. B ) )
11	10	ralrimiv	|- ( ph -> A. k e. NN0 ( F ` k ) e. B )
12		breq2	|- ( x = k -> ( S < x <-> S < k ) )
13		fveqeq2	|- ( x = k -> ( ( F ` x ) = .0. <-> ( F ` k ) = .0. ) )
14	12 13	imbi12d	|- ( x = k -> ( ( S < x -> ( F ` x ) = .0. ) <-> ( S < k -> ( F ` k ) = .0. ) ) )
15	14	cbvralvw	|- ( A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) <-> A. k e. NN0 ( S < k -> ( F ` k ) = .0. ) )
16	6 15	sylib	|- ( ph -> A. k e. NN0 ( S < k -> ( F ` k ) = .0. ) )
17	1 2 3 11 5 16	gsummptnn0fz	|- ( ph -> ( G gsum ( k e. NN0 |-> ( F ` k ) ) ) = ( G gsum ( k e. ( 0 ... S ) |-> ( F ` k ) ) ) )