Theorem gsummptnn0fz 16885

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 1683	. . . . 5 |- F/ x ( S < k -> C = .0. )
3		nfv 1683	. . . . . 6 |- F/ k S < x
4		nfcsb1v 3456	. . . . . . 7 |- F/_ k [_ x / k ]_ C
5	4	nfeq1 2644	. . . . . 6 |- F/ k [_ x / k ]_ C = .0.
6	3, 5	nfim 1867	. . . . 5 |- F/ k ( S < x -> [_ x / k ]_ C = .0. )
7		breq2 4457	. . . . . 6 |- ( k = x -> ( S < k <-> S < x ) )
8		csbeq1a 3449	. . . . . . 7 |- ( k = x -> C = [_ x / k ]_ C )
9	8	eqeq1d 2469	. . . . . 6 |- ( k = x -> ( C = .0. <-> [_ x / k ]_ C = .0. ) )
10	7, 9	imbi12d 320	. . . . 5 |- ( k = x -> ( ( S < k -> C = .0. ) <-> ( S < x -> [_ x / k ]_ C = .0. ) ) )
11	2, 6, 10	cbvral 3089	. . . 4 |- ( A. k e. NN0 ( S < k -> C = .0. ) <-> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
12	1, 11	sylib 196	. . 3 |- ( ph -> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
13		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ x e. NN0 ) -> x e. NN0 )
14		gsummptnn0fz.f	. . . . . . . . . . . . 13 |- ( ph -> A. k e. NN0 C e. B )
15	14	anim2i 569	. . . . . . . . . . . 12 |- ( ( x e. NN0 /\ ph ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
16	15	ancoms 453	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
17		rspcsbela 3858	. . . . . . . . . . 11 |- ( ( x e. NN0 /\ A. k e. NN0 C e. B ) -> [_ x / k ]_ C e. B )
18	16, 17	syl 16	. . . . . . . . . 10 |- ( ( ph /\ x e. NN0 ) -> [_ x / k ]_ C e. B )
19	13, 18	jca 532	. . . . . . . . 9 |- ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
20	19	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
21		eqid 2467	. . . . . . . . 9 |- ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
22	21	fvmpts 5959	. . . . . . . 8 |- ( ( x e. NN0 /\ [_ x / k ]_ C e. B ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
23	20, 22	syl 16	. . . . . . 7 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
24		simpr 461	. . . . . . 7 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> [_ x / k ]_ C = .0. )
25	23, 24	eqtrd 2508	. . . . . 6 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = .0. )
26	25	ex 434	. . . . 5 |- ( ( ph /\ x e. NN0 ) -> ( [_ x / k ]_ C = .0. -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) )
27	26	imim2d 52	. . . 4 |- ( ( ph /\ x e. NN0 ) -> ( ( S < x -> [_ x / k ]_ C = .0. ) -> ( S < x -> ( ( k e. NN0 |-> C ) ` x ) = .0. ) ) )
28	27	ralimdva 2875	. . 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 6053	. . . . 5 |- ( A. k e. NN0 C e. B <-> ( k e. NN0 |-> C ) : NN0 --> B )
34	14, 33	sylib 196	. . . 4 |- ( ph -> ( k e. NN0 |-> C ) : NN0 --> B )
35		fvex 5882	. . . . . . 7 |- ( Base ` G ) e. _V
36	30, 35	eqeltri 2551	. . . . . 6 |- B e. _V
37		nn0ex 10813	. . . . . 6 |- NN0 e. _V
38	36, 37	pm3.2i 455	. . . . 5 |- ( B e. _V /\ NN0 e. _V )
39		elmapg 7445	. . . . 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 12	. . . 4 |- ( ph -> ( ( k e. NN0 |-> C ) e. ( B ^m NN0 ) <-> ( k e. NN0 |-> C ) : NN0 --> B ) )
41	34, 40	mpbird 232	. . 3 |- ( ph -> ( k e. NN0 |-> C ) e. ( B ^m NN0 ) )
42		gsummptnn0fz.s	. . 3 |- ( ph -> S e. NN0 )
43		elfznn0 11782	. . . . . 6 |- ( k e. ( 0 ... S ) -> k e. NN0 )
44	43	ssriv 3513	. . . . 5 |- ( 0 ... S ) C_ NN0
45		resmpt 5329	. . . . 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 2480	. . 3 |- ( k e. ( 0 ... S ) |-> C ) = ( ( k e. NN0 |-> C ) |` ( 0 ... S ) )
48	30, 31, 32, 41, 42, 47	fsfnn0gsumfsffz 16882	. 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 184   /\ wa 369   = wceq 1379   F/wnf 1599   e. wcel 1767   A.wral 2817   _Vcvv 3118   [_csb 3440   C_ wss 3481   class class class wbr 4453   |-> cmpt 4511   |` cres 5007   -->wf 5590   ` cfv 5594  (class class class)co 6295   ^m cmap 7432   0cc0 9504   < clt 9640   NN0cn0 10807   ...cfz 11684   Basecbs 14506   0gc0g 14711   gsum_g cgsu 14712  CMndccmn 16669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-oi 7947  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-fzo 11805  df-seq 12088  df-hash 12386  df-0g 14713  df-gsum 14714  df-mgm 15745  df-sgrp 15784  df-mnd 15794  df-cntz 16226  df-cmn 16671

This theorem is referenced by:  gsummptnn0fzv  16886  gsummoncoe1  18214  pmatcollpwfi  19150