Theorem gsummptnn0fz 17663

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

Hypotheses

Ref	Expression
gsummptnn0fz.k	|- F/ k ph
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

Ref	Expression
gsummptnn0fz	|- ( ph -> ( G gsumg ( k e. NN0 |-> C ) ) = ( G gsumg ( k e. ( 0 ... S ) |-> C ) ) )

Distinct variable groups:   B, k   S, k   .0. , k

Allowed substitution hints:   ph( k)   C( k)   G( k)

Proof of Theorem gsummptnn0fz

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsummptnn0fz.u	. . . 4 |- ( ph -> A. k e. NN0 ( S < k -> C = .0. ) )
2		nfv 1771	. . . . 5 |- F/ x ( S < k -> C = .0. )
3		nfv 1771	. . . . . 6 |- F/ k S < x
4		nfcsb1v 3390	. . . . . . 7 |- F/_ k [_ x / k ]_ C
5	4	nfeq1 2615	. . . . . 6 |- F/ k [_ x / k ]_ C = .0.
6	3, 5	nfim 2013	. . . . 5 |- F/ k ( S < x -> [_ x / k ]_ C = .0. )
7		breq2 4419	. . . . . 6 |- ( k = x -> ( S < k <-> S < x ) )
8		csbeq1a 3383	. . . . . . 7 |- ( k = x -> C = [_ x / k ]_ C )
9	8	eqeq1d 2463	. . . . . 6 |- ( k = x -> ( C = .0. <-> [_ x / k ]_ C = .0. ) )
10	7, 9	imbi12d 326	. . . . 5 |- ( k = x -> ( ( S < k -> C = .0. ) <-> ( S < x -> [_ x / k ]_ C = .0. ) ) )
11	2, 6, 10	cbvral 3026	. . . 4 |- ( A. k e. NN0 ( S < k -> C = .0. ) <-> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
12	1, 11	sylib 201	. . 3 |- ( ph -> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
13		simpr 467	. . . . . . . . . 10 |- ( ( ph /\ x e. NN0 ) -> x e. NN0 )
14		gsummptnn0fz.f	. . . . . . . . . . . . 13 |- ( ph -> A. k e. NN0 C e. B )
15	14	anim2i 577	. . . . . . . . . . . 12 |- ( ( x e. NN0 /\ ph ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
16	15	ancoms 459	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
17		rspcsbela 3806	. . . . . . . . . . 11 |- ( ( x e. NN0 /\ A. k e. NN0 C e. B ) -> [_ x / k ]_ C e. B )
18	16, 17	syl 17	. . . . . . . . . 10 |- ( ( ph /\ x e. NN0 ) -> [_ x / k ]_ C e. B )
19	13, 18	jca 539	. . . . . . . . 9 |- ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
20	19	adantr 471	. . . . . . . 8 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
21		eqid 2461	. . . . . . . . 9 |- ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
22	21	fvmpts 5973	. . . . . . . 8 |- ( ( x e. NN0 /\ [_ x / k ]_ C e. B ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
23	20, 22	syl 17	. . . . . . 7 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
24		simpr 467	. . . . . . 7 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> [_ x / k ]_ C = .0. )
25	23, 24	eqtrd 2495	. . . . . 6 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = .0. )
26	25	ex 440	. . . . 5 |- ( ( ph /\ x e. NN0 ) -> ( [_ x / k ]_ C = .0. -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) )
27	26	imim2d 54	. . . 4 |- ( ( ph /\ x e. NN0 ) -> ( ( S < x -> [_ x / k ]_ C = .0. ) -> ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) ) )
28	27	ralimdva 2807	. . 3 |- ( ph -> ( A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) -> A. x e. NN0 ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) ) )
29	12, 28	mpd 15	. 2 |- ( ph -> A. x e. NN0 ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) )
30		gsummptnn0fz.b	. . 3 |- B = ( Base ` G )
31		gsummptnn0fz.0	. . 3 |- .0. = ( 0g ` G )
32		gsummptnn0fz.g	. . 3 |- ( ph -> G e. CMnd )
33	21	fmpt 6065	. . . . 5 |- ( A. k e. NN0 C e. B <-> ( k e. NN0 |-> C ) : NN0 --> B )
34	14, 33	sylib 201	. . . 4 |- ( ph -> ( k e. NN0 |-> C ) : NN0 --> B )
35		fvex 5897	. . . . . . 7 |- ( Base ` G ) e. _V
36	30, 35	eqeltri 2535	. . . . . 6 |- B e. _V
37		nn0ex 10903	. . . . . 6 |- NN0 e. _V
38	36, 37	pm3.2i 461	. . . . 5 |- ( B e. _V /\ NN0 e. _V )
39		elmapg 7510	. . . . 5 |- ( ( B e. _V /\ NN0 e. _V ) -> ( ( k e. NN0 |-> C ) e. ( B ^m NN0 ) <-> ( k e. NN0 |-> C ) : NN0 --> B ) )
40	38, 39	mp1i 13	. . . 4 |- ( ph -> ( ( k e. NN0 |-> C ) e. ( B ^m NN0 ) <-> ( k e. NN0 |-> C ) : NN0 --> B ) )
41	34, 40	mpbird 240	. . 3 |- ( ph -> ( k e. NN0 |-> C ) e. ( B ^m NN0 ) )
42		gsummptnn0fz.s	. . 3 |- ( ph -> S e. NN0 )
43		elfznn0 11915	. . . . . 6 |- ( k e. ( 0 ... S ) -> k e. NN0 )
44	43	ssriv 3447	. . . . 5 |- ( 0 ... S ) C_ NN0
45		resmpt 5172	. . . . 5 |- ( ( 0 ... S ) C_ NN0 -> ( ( k e. NN0 |-> C ) |` ( 0 ... S ) ) = ( k e. ( 0 ... S ) |-> C ) )
46	44, 45	ax-mp 5	. . . 4 |- ( ( k e. NN0 |-> C ) |` ( 0 ... S ) ) = ( k e. ( 0 ... S ) |-> C )
47	46	eqcomi 2470	. . 3 |- ( k e. ( 0 ... S ) |-> C ) = ( ( k e. NN0 |-> C ) |` ( 0 ... S ) )
48	30, 31, 32, 41, 42, 47	fsfnn0gsumfsffz 17660	. 2 |- ( ph -> ( A. x e. NN0 ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) -> ( G gsumg ( k e. NN0 |-> C ) ) = ( G gsumg ( k e. ( 0 ... S ) |-> C ) ) ) )
49	29, 48	mpd 15	1 |- ( ph -> ( G gsumg ( k e. NN0 |-> C ) ) = ( G gsumg ( k e. ( 0 ... S ) |-> C ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1454   F/wnf 1677   e. wcel 1897   A.wral 2748   _Vcvv 3056   [_csb 3374   C_ wss 3415   class class class wbr 4415   |-> cmpt 4474   |` cres 4854   -->wf 5596   ` cfv 5600  (class class class)co 6314   ^m cmap 7497   0cc0 9564   < clt 9700   NN0cn0 10897   ...cfz 11812   Basecbs 15169   0gc0g 15386   gsum_g cgsu 15387  CMndccmn 17478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-supp 6941  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-map 7499  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-fsupp 7909  df-oi 8050  df-card 8398  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-n0 10898  df-z 10966  df-uz 11188  df-fz 11813  df-fzo 11946  df-seq 12245  df-hash 12547  df-0g 15388  df-gsum 15389  df-mgm 16536  df-sgrp 16575  df-mnd 16585  df-cntz 17019  df-cmn 17480

This theorem is referenced by:  gsummptnn0fzv  17664  gsummoncoe1  18946  pmatcollpwfi  19854