Theorem gsum2d 16978

Description: Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)

Hypotheses

Ref	Expression
gsum2d.b	|- B = ( Base ` G )
gsum2d.z	|- .0. = ( 0g ` G )
gsum2d.g	|- ( ph -> G e. CMnd )
gsum2d.a	|- ( ph -> A e. V )
gsum2d.r	|- ( ph -> Rel A )
gsum2d.d	|- ( ph -> D e. W )
gsum2d.s	|- ( ph -> dom A C_ D )
gsum2d.f	|- ( ph -> F : A --> B )
gsum2d.w	|- ( ph -> F finSupp .0. )

Assertion

Ref	Expression
gsum2d	|- ( ph -> ( G gsumg F ) = ( G gsumg ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )

Distinct variable groups:   j, k, A   j, F, k   j, G, k   ph, j, k   B, j, k   D, j, k   .0. , j, k

Allowed substitution hints:   V( j, k)   W( j, k)

Proof of Theorem gsum2d

Step	Hyp	Ref	Expression
1		gsum2d.b	. . 3 |- B = ( Base ` G )
2		gsum2d.z	. . 3 |- .0. = ( 0g ` G )
3		gsum2d.g	. . 3 |- ( ph -> G e. CMnd )
4		gsum2d.a	. . 3 |- ( ph -> A e. V )
5		gsum2d.r	. . 3 |- ( ph -> Rel A )
6		gsum2d.d	. . 3 |- ( ph -> D e. W )
7		gsum2d.s	. . 3 |- ( ph -> dom A C_ D )
8		gsum2d.f	. . 3 |- ( ph -> F : A --> B )
9		gsum2d.w	. . 3 |- ( ph -> F finSupp .0. )
10	1, 2, 3, 4, 5, 6, 7, 8, 9	gsum2dlem2 16977	. 2 |- ( ph -> ( G gsumg ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsumg ( j e. dom ( F supp .0. ) |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
11		suppssdm 6916	. . . . . 6 |- ( F supp .0. ) C_ dom F
12		fdm 5725	. . . . . . 7 |- ( F : A --> B -> dom F = A )
13	8, 12	syl 16	. . . . . 6 |- ( ph -> dom F = A )
14	11, 13	syl5sseq 3537	. . . . 5 |- ( ph -> ( F supp .0. ) C_ A )
15		relss 5080	. . . . . . 7 |- ( ( F supp .0. ) C_ A -> ( Rel A -> Rel ( F supp .0. ) ) )
16	14, 5, 15	sylc 60	. . . . . 6 |- ( ph -> Rel ( F supp .0. ) )
17		relssdmrn 5518	. . . . . . 7 |- ( Rel ( F supp .0. ) -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) )
18		ssv 3509	. . . . . . . 8 |- ran ( F supp .0. ) C_ _V
19		xpss2 5102	. . . . . . . 8 |- ( ran ( F supp .0. ) C_ _V -> ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) C_ ( dom ( F supp .0. ) X. _V ) )
20	18, 19	ax-mp 5	. . . . . . 7 |- ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) C_ ( dom ( F supp .0. ) X. _V )
21	17, 20	syl6ss 3501	. . . . . 6 |- ( Rel ( F supp .0. ) -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. _V ) )
22	16, 21	syl 16	. . . . 5 |- ( ph -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. _V ) )
23	14, 22	ssind 3707	. . . 4 |- ( ph -> ( F supp .0. ) C_ ( A i^i ( dom ( F supp .0. ) X. _V ) ) )
24		df-res 5001	. . . 4 |- ( A |` dom ( F supp .0. ) ) = ( A i^i ( dom ( F supp .0. ) X. _V ) )
25	23, 24	syl6sseqr 3536	. . 3 |- ( ph -> ( F supp .0. ) C_ ( A |` dom ( F supp .0. ) ) )
26	1, 2, 3, 4, 8, 25, 9	gsumres 16900	. 2 |- ( ph -> ( G gsumg ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsumg F ) )
27		dmss 5192	. . . . . . 7 |- ( ( F supp .0. ) C_ A -> dom ( F supp .0. ) C_ dom A )
28	14, 27	syl 16	. . . . . 6 |- ( ph -> dom ( F supp .0. ) C_ dom A )
29	28, 7	sstrd 3499	. . . . 5 |- ( ph -> dom ( F supp .0. ) C_ D )
30	29	resmptd 5315	. . . 4 |- ( ph -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) |` dom ( F supp .0. ) ) = ( j e. dom ( F supp .0. ) |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
31	30	oveq2d 6297	. . 3 |- ( ph -> ( G gsumg ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) |` dom ( F supp .0. ) ) ) = ( G gsumg ( j e. dom ( F supp .0. ) |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
32	1, 2, 3, 4, 5, 6, 7, 8, 9	gsum2dlem1 16976	. . . . . 6 |- ( ph -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
33	32	adantr 465	. . . . 5 |- ( ( ph /\ j e. D ) -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
34		eqid 2443	. . . . 5 |- ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) )
35	33, 34	fmptd 6040	. . . 4 |- ( ph -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) : D --> B )
36		vex 3098	. . . . . . . . . . . . . 14 |- j e. _V
37		vex 3098	. . . . . . . . . . . . . 14 |- k e. _V
38	36, 37	elimasn 5352	. . . . . . . . . . . . 13 |- ( k e. ( A " { j } ) <-> <. j , k >. e. A )
39	38	biimpi 194	. . . . . . . . . . . 12 |- ( k e. ( A " { j } ) -> <. j , k >. e. A )
40	39	ad2antll 728	. . . . . . . . . . 11 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> <. j , k >. e. A )
41		eldifn 3612	. . . . . . . . . . . . 13 |- ( j e. ( D \ dom ( F supp .0. ) ) -> -. j e. dom ( F supp .0. ) )
42	41	ad2antrl 727	. . . . . . . . . . . 12 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> -. j e. dom ( F supp .0. ) )
43	36, 37	opeldm 5196	. . . . . . . . . . . 12 |- ( <. j , k >. e. ( F supp .0. ) -> j e. dom ( F supp .0. ) )
44	42, 43	nsyl 121	. . . . . . . . . . 11 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> -. <. j , k >. e. ( F supp .0. ) )
45	40, 44	eldifd 3472	. . . . . . . . . 10 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
46		df-ov 6284	. . . . . . . . . . 11 |- ( j F k ) = ( F ` <. j , k >. )
47		ssid 3508	. . . . . . . . . . . . 13 |- ( F supp .0. ) C_ ( F supp .0. )
48	47	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
49		fvex 5866	. . . . . . . . . . . . . 14 |- ( 0g ` G ) e. _V
50	2, 49	eqeltri 2527	. . . . . . . . . . . . 13 |- .0. e. _V
51	50	a1i 11	. . . . . . . . . . . 12 |- ( ph -> .0. e. _V )
52	8, 48, 4, 51	suppssr 6933	. . . . . . . . . . 11 |- ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
53	46, 52	syl5eq 2496	. . . . . . . . . 10 |- ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
54	45, 53	syldan 470	. . . . . . . . 9 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> ( j F k ) = .0. )
55	54	anassrs 648	. . . . . . . 8 |- ( ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) /\ k e. ( A " { j } ) ) -> ( j F k ) = .0. )
56	55	mpteq2dva 4523	. . . . . . 7 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { j } ) |-> .0. ) )
57	56	oveq2d 6297	. . . . . 6 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) )
58		cmnmnd 16792	. . . . . . . . 9 |- ( G e. CMnd -> G e. Mnd )
59	3, 58	syl 16	. . . . . . . 8 |- ( ph -> G e. Mnd )
60		imaexg 6722	. . . . . . . . 9 |- ( A e. V -> ( A " { j } ) e. _V )
61	4, 60	syl 16	. . . . . . . 8 |- ( ph -> ( A " { j } ) e. _V )
62	2	gsumz 15984	. . . . . . . 8 |- ( ( G e. Mnd /\ ( A " { j } ) e. _V ) -> ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
63	59, 61, 62	syl2anc 661	. . . . . . 7 |- ( ph -> ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
64	63	adantr 465	. . . . . 6 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
65	57, 64	eqtrd 2484	. . . . 5 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) = .0. )
66	65, 6	suppss2 6936	. . . 4 |- ( ph -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) C_ dom ( F supp .0. ) )
67		funmpt 5614	. . . . . 6 |- Fun ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) )
68	67	a1i 11	. . . . 5 |- ( ph -> Fun ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
69	9	fsuppimpd 7838	. . . . . . 7 |- ( ph -> ( F supp .0. ) e. Fin )
70		dmfi 7805	. . . . . . 7 |- ( ( F supp .0. ) e. Fin -> dom ( F supp .0. ) e. Fin )
71	69, 70	syl 16	. . . . . 6 |- ( ph -> dom ( F supp .0. ) e. Fin )
72		ssfi 7742	. . . . . 6 |- ( ( dom ( F supp .0. ) e. Fin /\ ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) C_ dom ( F supp .0. ) ) -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin )
73	71, 66, 72	syl2anc 661	. . . . 5 |- ( ph -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin )
74		mptexg 6127	. . . . . . 7 |- ( D e. W -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V )
75	6, 74	syl 16	. . . . . 6 |- ( ph -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V )
76		isfsupp 7835	. . . . . 6 |- ( ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V /\ .0. e. _V ) -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. <-> ( Fun ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) /\ ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin ) ) )
77	75, 51, 76	syl2anc 661	. . . . 5 |- ( ph -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. <-> ( Fun ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) /\ ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin ) ) )
78	68, 73, 77	mpbir2and 922	. . . 4 |- ( ph -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. )
79	1, 2, 3, 6, 35, 66, 78	gsumres 16900	. . 3 |- ( ph -> ( G gsumg ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) |` dom ( F supp .0. ) ) ) = ( G gsumg ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
80	31, 79	eqtr3d 2486	. 2 |- ( ph -> ( G gsumg ( j e. dom ( F supp .0. ) |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsumg ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
81	10, 26, 80	3eqtr3d 2492	1 |- ( ph -> ( G gsumg F ) = ( G gsumg ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1383   e. wcel 1804   _Vcvv 3095   \ cdif 3458   i^i cin 3460   C_ wss 3461   {csn 4014   <.cop 4020   class class class wbr 4437   |-> cmpt 4495   X. cxp 4987   dom cdm 4989   ran crn 4990   |` cres 4991   "cima 4992   Rel wrel 4994   Fun wfun 5572   -->wf 5574   ` cfv 5578  (class class class)co 6281   supp csupp 6903   Fincfn 7518   finSupp cfsupp 7831   Basecbs 14614   0gc0g 14819   gsum_g cgsu 14820   Mndcmnd 15898  CMndccmn 16777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-inf2 8061  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6904  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-fsupp 7832  df-oi 7938  df-card 8323  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-2 10601  df-n0 10803  df-z 10872  df-uz 11093  df-fz 11684  df-fzo 11807  df-seq 12090  df-hash 12388  df-ndx 14617  df-slot 14618  df-base 14619  df-sets 14620  df-ress 14621  df-plusg 14692  df-0g 14821  df-gsum 14822  df-mre 14965  df-mrc 14966  df-acs 14968  df-mgm 15851  df-sgrp 15890  df-mnd 15900  df-submnd 15946  df-mulg 16039  df-cntz 16334  df-cmn 16779

This theorem is referenced by:  gsum2d2  16981  gsumxp  16983