Metamath Proof Explorer

Theorem nn0gsumfz

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

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 2 fvexi 
 |-  .0. e. _V
7 4 6 jctir 
 |-  ( ph -> ( F e. ( B ^m NN0 ) /\ .0. e. _V ) )
8 fsuppmapnn0ub 
 |-  ( ( F e. ( B ^m NN0 ) /\ .0. e. _V ) -> ( F finSupp .0. -> E. s e. NN0 A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) )
9 7 5 8 sylc 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) )
10 eqidd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> ( F |` ( 0 ... s ) ) = ( F |` ( 0 ... s ) ) )
11 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) )
12 3 adantr 
 |-  ( ( ph /\ s e. NN0 ) -> G e. CMnd )
13 4 adantr 
 |-  ( ( ph /\ s e. NN0 ) -> F e. ( B ^m NN0 ) )
14 simpr 
 |-  ( ( ph /\ s e. NN0 ) -> s e. NN0 )
15 eqid 
 |-  ( F |` ( 0 ... s ) ) = ( F |` ( 0 ... s ) )
16 1 2 12 13 14 15 fsfnn0gsumfsffz 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) -> ( G gsum F ) = ( G gsum ( F |` ( 0 ... s ) ) ) ) )
17 16 imp 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> ( G gsum F ) = ( G gsum ( F |` ( 0 ... s ) ) ) )
18 13 adantr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> F e. ( B ^m NN0 ) )
19 fz0ssnn0 
 |-  ( 0 ... s ) C_ NN0
20 elmapssres 
 |-  ( ( F e. ( B ^m NN0 ) /\ ( 0 ... s ) C_ NN0 ) -> ( F |` ( 0 ... s ) ) e. ( B ^m ( 0 ... s ) ) )
21 18 19 20 sylancl 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> ( F |` ( 0 ... s ) ) e. ( B ^m ( 0 ... s ) ) )
22 eqeq1 
 |-  ( f = ( F |` ( 0 ... s ) ) -> ( f = ( F |` ( 0 ... s ) ) <-> ( F |` ( 0 ... s ) ) = ( F |` ( 0 ... s ) ) ) )
23 oveq2 
 |-  ( f = ( F |` ( 0 ... s ) ) -> ( G gsum f ) = ( G gsum ( F |` ( 0 ... s ) ) ) )
24 23 eqeq2d 
 |-  ( f = ( F |` ( 0 ... s ) ) -> ( ( G gsum F ) = ( G gsum f ) <-> ( G gsum F ) = ( G gsum ( F |` ( 0 ... s ) ) ) ) )
25 22 24 3anbi13d 
 |-  ( f = ( F |` ( 0 ... s ) ) -> ( ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum f ) ) <-> ( ( F |` ( 0 ... s ) ) = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum ( F |` ( 0 ... s ) ) ) ) ) )
26 25 adantl 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) /\ f = ( F |` ( 0 ... s ) ) ) -> ( ( f = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum f ) ) <-> ( ( F |` ( 0 ... s ) ) = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum ( F |` ( 0 ... s ) ) ) ) ) )
27 21 26 rspcedv 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> ( ( ( F |` ( 0 ... s ) ) = ( F |` ( 0 ... s ) ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) /\ ( G gsum F ) = ( G gsum ( F |` ( 0 ... s ) ) ) ) -> 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 ) ) ) )
28 10 11 17 27 mp3and 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) ) -> 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 ) ) )
29 28 ex 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) -> 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 ) ) ) )
30 29 reximdva 
 |-  ( ph -> ( E. s e. NN0 A. x e. NN0 ( s < x -> ( F ` x ) = .0. ) -> 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 ) ) ) )
31 9 30 mpd 
 |-  ( 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 ) ) )