Theorem gsum2d 16439

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 16438	. 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 6694	. . . . . 6 |- ( F supp .0. ) C_ dom F
12		fdm 5553	. . . . . . 7 |- ( F : A --> B -> dom F = A )
13	8, 12	syl 16	. . . . . 6 |- ( ph -> dom F = A )
14	11, 13	syl5sseq 3394	. . . . 5 |- ( ph -> ( F supp .0. ) C_ A )
15		relss 4916	. . . . . . 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 5348	. . . . . . 7 |- ( Rel ( F supp .0. ) -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) )
18		ssv 3366	. . . . . . . 8 |- ran ( F supp .0. ) C_ _V
19		xpss2 4938	. . . . . . . 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 3358	. . . . . 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 3564	. . . 4 |- ( ph -> ( F supp .0. ) C_ ( A i^i ( dom ( F supp .0. ) X. _V ) ) )
24		df-res 4841	. . . 4 |- ( A |` dom ( F supp .0. ) ) = ( A i^i ( dom ( F supp .0. ) X. _V ) )
25	23, 24	syl6sseqr 3393	. . 3 |- ( ph -> ( F supp .0. ) C_ ( A |` dom ( F supp .0. ) ) )
26	1, 2, 3, 4, 8, 25, 9	gsumres 16377	. 2 |- ( ph -> ( G gsumg ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsumg F ) )
27		dmss 5028	. . . . . . 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 3356	. . . . 5 |- ( ph -> dom ( F supp .0. ) C_ D )
30		resmpt 5146	. . . . 5 |- ( dom ( F supp .0. ) C_ D -> ( ( 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	29, 30	syl 16	. . . 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 ) ) ) ) )
32	31	oveq2d 6098	. . 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 ) ) ) ) ) )
33	1, 2, 3, 4, 5, 6, 7, 8, 9	gsum2dlem1 16437	. . . . . 6 |- ( ph -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
34	33	adantr 462	. . . . 5 |- ( ( ph /\ j e. D ) -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
35		eqid 2435	. . . . 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 ) ) ) )
36	34, 35	fmptd 5857	. . . 4 |- ( ph -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) : D --> B )
37		vex 2967	. . . . . . . . . . . . . 14 |- j e. _V
38		vex 2967	. . . . . . . . . . . . . 14 |- k e. _V
39	37, 38	elimasn 5184	. . . . . . . . . . . . 13 |- ( k e. ( A " { j } ) <-> <. j , k >. e. A )
40	39	biimpi 194	. . . . . . . . . . . 12 |- ( k e. ( A " { j } ) -> <. j , k >. e. A )
41	40	ad2antll 723	. . . . . . . . . . 11 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> <. j , k >. e. A )
42		eldifn 3469	. . . . . . . . . . . . 13 |- ( j e. ( D \ dom ( F supp .0. ) ) -> -. j e. dom ( F supp .0. ) )
43	42	ad2antrl 722	. . . . . . . . . . . 12 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> -. j e. dom ( F supp .0. ) )
44	37, 38	opeldm 5032	. . . . . . . . . . . 12 |- ( <. j , k >. e. ( F supp .0. ) -> j e. dom ( F supp .0. ) )
45	43, 44	nsyl 121	. . . . . . . . . . 11 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> -. <. j , k >. e. ( F supp .0. ) )
46	41, 45	eldifd 3329	. . . . . . . . . 10 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
47		df-ov 6085	. . . . . . . . . . 11 |- ( j F k ) = ( F ` <. j , k >. )
48		ssid 3365	. . . . . . . . . . . . 13 |- ( F supp .0. ) C_ ( F supp .0. )
49	48	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
50		fvex 5691	. . . . . . . . . . . . . 14 |- ( 0g ` G ) e. _V
51	2, 50	eqeltri 2505	. . . . . . . . . . . . 13 |- .0. e. _V
52	51	a1i 11	. . . . . . . . . . . 12 |- ( ph -> .0. e. _V )
53	8, 49, 4, 52	suppssr 6711	. . . . . . . . . . 11 |- ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
54	47, 53	syl5eq 2479	. . . . . . . . . 10 |- ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
55	46, 54	syldan 467	. . . . . . . . 9 |- ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> ( j F k ) = .0. )
56	55	anassrs 643	. . . . . . . 8 |- ( ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) /\ k e. ( A " { j } ) ) -> ( j F k ) = .0. )
57	56	mpteq2dva 4368	. . . . . . 7 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { j } ) |-> .0. ) )
58	57	oveq2d 6098	. . . . . 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. ) ) )
59		cmnmnd 16274	. . . . . . . . 9 |- ( G e. CMnd -> G e. Mnd )
60	3, 59	syl 16	. . . . . . . 8 |- ( ph -> G e. Mnd )
61		imaexg 6506	. . . . . . . . 9 |- ( A e. V -> ( A " { j } ) e. _V )
62	4, 61	syl 16	. . . . . . . 8 |- ( ph -> ( A " { j } ) e. _V )
63	2	gsumz 15493	. . . . . . . 8 |- ( ( G e. Mnd /\ ( A " { j } ) e. _V ) -> ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
64	60, 62, 63	syl2anc 656	. . . . . . 7 |- ( ph -> ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
65	64	adantr 462	. . . . . 6 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsumg ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
66	58, 65	eqtrd 2467	. . . . 5 |- ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) = .0. )
67	66, 6	suppss2 6714	. . . 4 |- ( ph -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) C_ dom ( F supp .0. ) )
68		funmpt 5444	. . . . . 6 |- Fun ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) )
69	68	a1i 11	. . . . 5 |- ( ph -> Fun ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
70	9	fsuppimpd 7617	. . . . . . 7 |- ( ph -> ( F supp .0. ) e. Fin )
71		dmfi 7584	. . . . . . 7 |- ( ( F supp .0. ) e. Fin -> dom ( F supp .0. ) e. Fin )
72	70, 71	syl 16	. . . . . 6 |- ( ph -> dom ( F supp .0. ) e. Fin )
73		ssfi 7523	. . . . . 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 )
74	72, 67, 73	syl2anc 656	. . . . 5 |- ( ph -> ( ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin )
75		mptexg 5936	. . . . . . 7 |- ( D e. W -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V )
76	6, 75	syl 16	. . . . . 6 |- ( ph -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V )
77		isfsupp 7614	. . . . . 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 ) ) )
78	76, 52, 77	syl2anc 656	. . . . 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 ) ) )
79	69, 74, 78	mpbir2and 908	. . . 4 |- ( ph -> ( j e. D |-> ( G gsumg ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. )
80	1, 2, 3, 6, 36, 67, 79	gsumres 16377	. . 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 ) ) ) ) ) )
81	32, 80	eqtr3d 2469	. 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 ) ) ) ) ) )
82	10, 26, 81	3eqtr3d 2475	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 1364   e. wcel 1757   _Vcvv 2964   \ cdif 3315   i^i cin 3317   C_ wss 3318   {csn 3867   <.cop 3873   class class class wbr 4282   e. cmpt 4340   X. cxp 4827   dom cdm 4829   ran crn 4830   |` cres 4831   "cima 4832   Rel wrel 4834   Fun wfun 5402   -->wf 5404   ` cfv 5408  (class class class)co 6082   supp csupp 6681   Fincfn 7300   finSupp cfsupp 7610   Basecbs 14159   0gc0g 14363   gsum_g cgsu 14364   Mndcmnd 15394  CMndccmn 16259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-inf2 7837  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-iin 4164  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-se 4669  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6311  df-om 6468  df-1st 6568  df-2nd 6569  df-supp 6682  df-recs 6820  df-rdg 6854  df-1o 6910  df-oadd 6914  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-fsupp 7611  df-oi 7714  df-card 8099  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313  df-2 10370  df-n0 10570  df-z 10637  df-uz 10852  df-fz 11427  df-fzo 11535  df-seq 11793  df-hash 12090  df-ndx 14162  df-slot 14163  df-base 14164  df-sets 14165  df-ress 14166  df-plusg 14236  df-0g 14365  df-gsum 14366  df-mre 14509  df-mrc 14510  df-acs 14512  df-mnd 15400  df-submnd 15450  df-mulg 15530  df-cntz 15817  df-cmn 16261

This theorem is referenced by:  gsum2d2  16442  gsumxp  16444