Metamath Proof Explorer

Theorem fsfnn0gsumfsffz

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 ) )
fsfnn0gsumfsffz.s 
|- ( ph -> S e. NN0 )
fsfnn0gsumfsffz.h 
|- H = ( F |` ( 0 ... S ) )
Assertion fsfnn0gsumfsffz 
|- ( ph -> ( A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) -> ( G gsum F ) = ( G gsum H ) ) )

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 fsfnn0gsumfsffz.s 
 |-  ( ph -> S e. NN0 )
6 fsfnn0gsumfsffz.h 
 |-  H = ( F |` ( 0 ... S ) )
7 6 oveq2i 
 |-  ( G gsum H ) = ( G gsum ( F |` ( 0 ... S ) ) )
8 3 adantr 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> G e. CMnd )
9 nn0ex 
 |-  NN0 e. _V
10 9 a1i 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> NN0 e. _V )
11 elmapi 
 |-  ( F e. ( B ^m NN0 ) -> F : NN0 --> B )
12 4 11 syl 
 |-  ( ph -> F : NN0 --> B )
13 12 adantr 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> F : NN0 --> B )
14 2 fvexi 
 |-  .0. e. _V
15 14 a1i 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> .0. e. _V )
16 4 adantr 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> F e. ( B ^m NN0 ) )
17 5 adantr 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> S e. NN0 )
18 simpr 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) )
19 15 16 17 18 suppssfz 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> ( F supp .0. ) C_ ( 0 ... S ) )
20 elmapfun 
 |-  ( F e. ( B ^m NN0 ) -> Fun F )
21 4 20 syl 
 |-  ( ph -> Fun F )
22 14 a1i 
 |-  ( ph -> .0. e. _V )
23 4 21 22 3jca 
 |-  ( ph -> ( F e. ( B ^m NN0 ) /\ Fun F /\ .0. e. _V ) )
24 fzfid 
 |-  ( ph -> ( 0 ... S ) e. Fin )
25 24 anim1i 
 |-  ( ( ph /\ ( F supp .0. ) C_ ( 0 ... S ) ) -> ( ( 0 ... S ) e. Fin /\ ( F supp .0. ) C_ ( 0 ... S ) ) )
26 suppssfifsupp 
 |-  ( ( ( F e. ( B ^m NN0 ) /\ Fun F /\ .0. e. _V ) /\ ( ( 0 ... S ) e. Fin /\ ( F supp .0. ) C_ ( 0 ... S ) ) ) -> F finSupp .0. )
27 23 25 26 syl2an2r 
 |-  ( ( ph /\ ( F supp .0. ) C_ ( 0 ... S ) ) -> F finSupp .0. )
28 19 27 syldan 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> F finSupp .0. )
29 1 2 8 10 13 19 28 gsumres 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> ( G gsum ( F |` ( 0 ... S ) ) ) = ( G gsum F ) )
30 7 29 eqtr2id 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) ) -> ( G gsum F ) = ( G gsum H ) )
31 30 ex 
 |-  ( ph -> ( A. x e. NN0 ( S < x -> ( F ` x ) = .0. ) -> ( G gsum F ) = ( G gsum H ) ) )