This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdm 
 |-  ( ( 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 ) ) ) )