Theorem gsummptnn0fz 17558

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 1755	. . . . 5 |- F/ x ( S < k -> C = .0. )
3		nfv 1755	. . . . . 6 |- F/ k S < x
4		nfcsb1v 3354	. . . . . . 7 |- F/_ k [_ x / k ]_ C
5	4	nfeq1 2582	. . . . . 6 |- F/ k [_ x / k ]_ C = .0.
6	3, 5	nfim 1980	. . . . 5 |- F/ k ( S < x -> [_ x / k ]_ C = .0. )
7		breq2 4370	. . . . . 6 |- ( k = x -> ( S < k <-> S < x ) )
8		csbeq1a 3347	. . . . . . 7 |- ( k = x -> C = [_ x / k ]_ C )
9	8	eqeq1d 2430	. . . . . 6 |- ( k = x -> ( C = .0. <-> [_ x / k ]_ C = .0. ) )
10	7, 9	imbi12d 321	. . . . 5 |- ( k = x -> ( ( S < k -> C = .0. ) <-> ( S < x -> [_ x / k ]_ C = .0. ) ) )
11	2, 6, 10	cbvral 2992	. . . 4 |- ( A. k e. NN0 ( S < k -> C = .0. ) <-> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
12	1, 11	sylib 199	. . 3 |- ( ph -> A. x e. NN0 ( S < x -> [_ x / k ]_ C = .0. ) )
13		simpr 462	. . . . . . . . . 10 |- ( ( ph /\ x e. NN0 ) -> x e. NN0 )
14		gsummptnn0fz.f	. . . . . . . . . . . . 13 |- ( ph -> A. k e. NN0 C e. B )
15	14	anim2i 571	. . . . . . . . . . . 12 |- ( ( x e. NN0 /\ ph ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
16	15	ancoms 454	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ A. k e. NN0 C e. B ) )
17		rspcsbela 3768	. . . . . . . . . . 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 534	. . . . . . . . 9 |- ( ( ph /\ x e. NN0 ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
20	19	adantr 466	. . . . . . . 8 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( x e. NN0 /\ [_ x / k ]_ C e. B ) )
21		eqid 2428	. . . . . . . . 9 |- ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
22	21	fvmpts 5911	. . . . . . . 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 462	. . . . . . 7 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> [_ x / k ]_ C = .0. )
25	23, 24	eqtrd 2462	. . . . . 6 |- ( ( ( ph /\ x e. NN0 ) /\ [_ x / k ]_ C = .0. ) -> ( ( k e. NN0 |-> C ) ` x ) = .0. )
26	25	ex 435	. . . . 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 2773	. . 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 6002	. . . . 5 |- ( A. k e. NN0 C e. B <-> ( k e. NN0 |-> C ) : NN0 --> B )
34	14, 33	sylib 199	. . . 4 |- ( ph -> ( k e. NN0 |-> C ) : NN0 --> B )
35		fvex 5835	. . . . . . 7 |- ( Base ` G ) e. _V
36	30, 35	eqeltri 2502	. . . . . 6 |- B e. _V
37		nn0ex 10826	. . . . . 6 |- NN0 e. _V
38	36, 37	pm3.2i 456	. . . . 5 |- ( B e. _V /\ NN0 e. _V )
39		elmapg 7440	. . . . 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 235	. . 3 |- ( ph -> ( k e. NN0 |-> C ) e. ( B ^m NN0 ) )
42		gsummptnn0fz.s	. . 3 |- ( ph -> S e. NN0 )
43		elfznn0 11838	. . . . . 6 |- ( k e. ( 0 ... S ) -> k e. NN0 )
44	43	ssriv 3411	. . . . 5 |- ( 0 ... S ) C_ NN0
45		resmpt 5116	. . . . 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 2437	. . 3 |- ( k e. ( 0 ... S ) |-> C ) = ( ( k e. NN0 |-> C ) |` ( 0 ... S ) )
48	30, 31, 32, 41, 42, 47	fsfnn0gsumfsffz 17555	. 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 187   /\ wa 370   = wceq 1437   F/wnf 1661   e. wcel 1872   A.wral 2714   _Vcvv 3022   [_csb 3338   C_ wss 3379   class class class wbr 4366   |-> cmpt 4425   |` cres 4798   -->wf 5540   ` cfv 5544  (class class class)co 6249   ^m cmap 7427   0cc0 9490   < clt 9626   NN0cn0 10820   ...cfz 11735   Basecbs 15064   0gc0g 15281   gsum_g cgsu 15282  CMndccmn 17373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-se 4756  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-isom 5553  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-supp 6870  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-fsupp 7837  df-oi 7978  df-card 8325  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-n0 10821  df-z 10889  df-uz 11111  df-fz 11736  df-fzo 11867  df-seq 12164  df-hash 12466  df-0g 15283  df-gsum 15284  df-mgm 16431  df-sgrp 16470  df-mnd 16480  df-cntz 16914  df-cmn 17375

This theorem is referenced by:  gsummptnn0fzv  17559  gsummoncoe1  18841  pmatcollpwfi  19748