Metamath Proof Explorer

Theorem gsummptnn0fz

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

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

Proof

Step Hyp Ref Expression
1 gsummptnn0fz.b 
 |-  B = ( Base ` G )
2 gsummptnn0fz.0 
 |-  .0. = ( 0g ` G )
3 gsummptnn0fz.g 
 |-  ( ph -> G e. CMnd )
4 gsummptnn0fz.f 
 |-  ( ph -> A. k e. NN0 C e. B )
5 gsummptnn0fz.s 
 |-  ( ph -> S e. NN0 )
6 gsummptnn0fz.u 
 |-  ( ph -> A. k e. NN0 ( S < k -> C = .0. ) )
7 nfv 
 |-  F/ x ( S < k -> C = .0. )
8 nfv 
 |-  F/ k S < x
9 nfcsb1v 
 |-  F/_ k [_ x / k ]_ C
10 9 nfeq1 
 |-  F/ k [_ x / k ]_ C = .0.
11 8 10 nfim 
 |-  F/ k ( S < x -> [_ x / k ]_ C = .0. )
12 breq2 
 |-  ( k = x -> ( S < k <-> S < x ) )
13 csbeq1a 
 |-  ( k = x -> C = [_ x / k ]_ C )
14 13 eqeq1d 
 |-  ( k = x -> ( C = .0. <-> [_ x / k ]_ C = .0. ) )
15 12 14 imbi12d 
 |-  ( k = x -> ( ( S < k -> C = .0. ) <-> ( S < x -> [_ x / k ]_ C = .0. ) ) )
16 7 11 15 cbvralw 
 |-  ( A. k e. NN0 ( S < k -> C = .0. ) <-> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
17 6 16 sylib 
 |-  ( ph -> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
18 simpr 
 |-  ( ( ph /\ x e. NN0 ) -> x e. NN0 )
19 4 anim1ci 
 |-  ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
20 rspcsbela 
 |-  ( ( x e. NN0 /\ A. k e. NN0 C e. B ) -> [_ x / k ]_ C e. B )
21 19 20 syl 
 |-  ( ( ph /\ x e. NN0 ) -> [_ x / k ]_ C e. B )
22 18 21 jca 
 |-  ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
23 22 adantr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
24 eqid 
 |-  ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
25 24 fvmpts 
 |-  ( ( x e. NN0 /\ [_ x / k ]_ C e. B ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
26 23 25 syl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
27 simpr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> [_ x / k ]_ C = .0. )
28 26 27 eqtrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = .0. )
29 28 ex 
 |-  ( ( ph /\ x e. NN0 ) -> ( [_ x / k ]_ C = .0. -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) )
30 29 imim2d 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( S < x -> [_ x / k ]_ C = .0. ) -> ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) ) )
31 30 ralimdva 
 |-  ( ph -> ( A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) -> A. x e. NN0 ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) ) )
32 17 31 mpd 
 |-  ( ph -> A. x e. NN0 ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) )
33 24 fmpt 
 |-  ( A. k e. NN0 C e. B <-> ( k e. NN0 |-> C ) : NN0 --> B )
34 4 33 sylib 
 |-  ( ph -> ( k e. NN0 |-> C ) : NN0 --> B )
35 1 fvexi 
 |-  B e. _V
36 nn0ex 
 |-  NN0 e. _V
37 35 36 pm3.2i 
 |-  ( B e. _V /\ NN0 e. _V )
38 elmapg 
 |-  ( ( B e. _V /\ NN0 e. _V ) -> ( ( k e. NN0 |-> C ) e. ( B ^m NN0 ) <-> ( k e. NN0 |-> C ) : NN0 --> B ) )
39 37 38 mp1i 
 |-  ( ph -> ( ( k e. NN0 |-> C ) e. ( B ^m NN0 ) <-> ( k e. NN0 |-> C ) : NN0 --> B ) )
40 34 39 mpbird 
 |-  ( ph -> ( k e. NN0 |-> C ) e. ( B ^m NN0 ) )
41 fz0ssnn0 
 |-  ( 0 ... S ) C_ NN0
42 resmpt 
 |-  ( ( 0 ... S ) C_ NN0 -> ( ( k e. NN0 |-> C ) |` ( 0 ... S ) ) = ( k e. ( 0 ... S ) |-> C ) )
43 41 42 ax-mp 
 |-  ( ( k e. NN0 |-> C ) |` ( 0 ... S ) ) = ( k e. ( 0 ... S ) |-> C )
44 43 eqcomi 
 |-  ( k e. ( 0 ... S ) |-> C ) = ( ( k e. NN0 |-> C ) |` ( 0 ... S ) )
45 1 2 3 40 5 44 fsfnn0gsumfsffz 
 |-  ( ph -> ( A. x e. NN0 ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) -> ( G gsum ( k e. NN0 |-> C ) ) = ( G gsum ( k e. ( 0 ... S ) |-> C ) ) ) )
46 32 45 mpd 
 |-  ( ph -> ( G gsum ( k e. NN0 |-> C ) ) = ( G gsum ( k e. ( 0 ... S ) |-> C ) ) )