Theorem gsum2d2 17617

Description: Write a group sum over a two-dimensional region as a double sum. (Note that C ( j ) is a function of j.) (Contributed by Mario Carneiro, 28-Dec-2014.)

Hypotheses

Ref	Expression
gsum2d2.b	|- B = ( Base ` G )
gsum2d2.z	|- .0. = ( 0g ` G )
gsum2d2.g	|- ( ph -> G e. CMnd )
gsum2d2.a	|- ( ph -> A e. V )
gsum2d2.r	|- ( ( ph /\ j e. A ) -> C e. W )
gsum2d2.f	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
gsum2d2.u	|- ( ph -> U e. Fin )
gsum2d2.n	|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )

Assertion

Ref	Expression
gsum2d2	|- ( ph -> ( G gsumg ( j e. A , k e. C |-> X ) ) = ( G gsumg ( j e. A |-> ( G gsumg ( k e. C |-> X ) ) ) ) )

Distinct variable groups:   j, k, B   ph, j, k   A, j, k   j, G, k   U, j, k   C, k   j, V   .0. , j, k

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

Proof of Theorem gsum2d2

Dummy variables m n x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsum2d2.b	. . 3 |- B = ( Base ` G )
2		gsum2d2.z	. . 3 |- .0. = ( 0g ` G )
3		gsum2d2.g	. . 3 |- ( ph -> G e. CMnd )
4		gsum2d2.a	. . . 4 |- ( ph -> A e. V )
5		snex 4614	. . . . . 6 |- { j } e. _V
6		gsum2d2.r	. . . . . 6 |- ( ( ph /\ j e. A ) -> C e. W )
7		xpexg 6581	. . . . . 6 |- ( ( { j } e. _V /\ C e. W ) -> ( { j } X. C ) e. _V )
8	5, 6, 7	sylancr 674	. . . . 5 |- ( ( ph /\ j e. A ) -> ( { j } X. C ) e. _V )
9	8	ralrimiva 2790	. . . 4 |- ( ph -> A. j e. A ( { j } X. C ) e. _V )
10		iunexg 6757	. . . 4 |- ( ( A e. V /\ A. j e. A ( { j } X. C ) e. _V ) -> U_ j e. A ( { j } X. C ) e. _V )
11	4, 9, 10	syl2anc 671	. . 3 |- ( ph -> U_ j e. A ( { j } X. C ) e. _V )
12		relxp 4920	. . . . . 6 |- Rel ( { j } X. C )
13	12	rgenw 2749	. . . . 5 |- A. j e. A Rel ( { j } X. C )
14		reliun 4932	. . . . 5 |- ( Rel U_ j e. A ( { j } X. C ) <-> A. j e. A Rel ( { j } X. C ) )
15	13, 14	mpbir 214	. . . 4 |- Rel U_ j e. A ( { j } X. C )
16	15	a1i 11	. . 3 |- ( ph -> Rel U_ j e. A ( { j } X. C ) )
17		vex 3016	. . . . . 6 |- x e. _V
18	17	eldm2 5011	. . . . 5 |- ( x e. dom U_ j e. A ( { j } X. C ) <-> E. y <. x , y >. e. U_ j e. A ( { j } X. C ) )
19		eliunxp 4950	. . . . . . 7 |- ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) )
20		vex 3016	. . . . . . . . . . . 12 |- y e. _V
21	17, 20	opth1 4648	. . . . . . . . . . 11 |- ( <. x , y >. = <. j , k >. -> x = j )
22	21	ad2antrl 739	. . . . . . . . . 10 |- ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> x = j )
23		simprrl 779	. . . . . . . . . 10 |- ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> j e. A )
24	22, 23	eqeltrd 2530	. . . . . . . . 9 |- ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> x e. A )
25	24	ex 440	. . . . . . . 8 |- ( ph -> ( ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) -> x e. A ) )
26	25	exlimdvv 1784	. . . . . . 7 |- ( ph -> ( E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) -> x e. A ) )
27	19, 26	syl5bi 225	. . . . . 6 |- ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. C ) -> x e. A ) )
28	27	exlimdv 1783	. . . . 5 |- ( ph -> ( E. y <. x , y >. e. U_ j e. A ( { j } X. C ) -> x e. A ) )
29	18, 28	syl5bi 225	. . . 4 |- ( ph -> ( x e. dom U_ j e. A ( { j } X. C ) -> x e. A ) )
30	29	ssrdv 3406	. . 3 |- ( ph -> dom U_ j e. A ( { j } X. C ) C_ A )
31		gsum2d2.f	. . . . 5 |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
32	31	ralrimivva 2795	. . . 4 |- ( ph -> A. j e. A A. k e. C X e. B )
33		eqid 2452	. . . . 5 |- ( j e. A , k e. C |-> X ) = ( j e. A , k e. C |-> X )
34	33	fmpt2x 6847	. . . 4 |- ( A. j e. A A. k e. C X e. B <-> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
35	32, 34	sylib 201	. . 3 |- ( ph -> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
36		gsum2d2.u	. . . 4 |- ( ph -> U e. Fin )
37		gsum2d2.n	. . . 4 |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
38	1, 2, 3, 4, 6, 31, 36, 37	gsum2d2lem 17616	. . 3 |- ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. )
39	1, 2, 3, 11, 16, 4, 30, 35, 38	gsum2d 17615	. 2 |- ( ph -> ( G gsumg ( j e. A , k e. C |-> X ) ) = ( G gsumg ( m e. A |-> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) ) )
40		nfcv 2593	. . . . . 6 |- F/_ j G
41		nfcv 2593	. . . . . 6 |- F/_ j gsumg
42		nfiu1 4278	. . . . . . . 8 |- F/_ j U_ j e. A ( { j } X. C )
43		nfcv 2593	. . . . . . . 8 |- F/_ j { m }
44	42, 43	nfima 5154	. . . . . . 7 |- F/_ j ( U_ j e. A ( { j } X. C ) " { m } )
45		nfcv 2593	. . . . . . . 8 |- F/_ j m
46		nfmpt21 6346	. . . . . . . 8 |- F/_ j ( j e. A , k e. C |-> X )
47		nfcv 2593	. . . . . . . 8 |- F/_ j n
48	45, 46, 47	nfov 6302	. . . . . . 7 |- F/_ j ( m ( j e. A , k e. C |-> X ) n )
49	44, 48	nfmpt 4463	. . . . . 6 |- F/_ j ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) )
50	40, 41, 49	nfov 6302	. . . . 5 |- F/_ j ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) )
51		nfcv 2593	. . . . 5 |- F/_ m ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) )
52		sneq 3946	. . . . . . . 8 |- ( m = j -> { m } = { j } )
53	52	imaeq2d 5146	. . . . . . 7 |- ( m = j -> ( U_ j e. A ( { j } X. C ) " { m } ) = ( U_ j e. A ( { j } X. C ) " { j } ) )
54		oveq1 6283	. . . . . . 7 |- ( m = j -> ( m ( j e. A , k e. C |-> X ) n ) = ( j ( j e. A , k e. C |-> X ) n ) )
55	53, 54	mpteq12dv 4453	. . . . . 6 |- ( m = j -> ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) = ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) )
56	55	oveq2d 6292	. . . . 5 |- ( m = j -> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) = ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) )
57	50, 51, 56	cbvmpt 4466	. . . 4 |- ( m e. A |-> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) )
58		vex 3016	. . . . . . . . . . . . . 14 |- j e. _V
59		vex 3016	. . . . . . . . . . . . . 14 |- k e. _V
60	58, 59	elimasn 5171	. . . . . . . . . . . . 13 |- ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> <. j , k >. e. U_ j e. A ( { j } X. C ) )
61		opeliunxp 4864	. . . . . . . . . . . . 13 |- ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> ( j e. A /\ k e. C ) )
62	60, 61	bitri 257	. . . . . . . . . . . 12 |- ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> ( j e. A /\ k e. C ) )
63	62	baib 916	. . . . . . . . . . 11 |- ( j e. A -> ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> k e. C ) )
64	63	eqrdv 2450	. . . . . . . . . 10 |- ( j e. A -> ( U_ j e. A ( { j } X. C ) " { j } ) = C )
65	64	mpteq1d 4456	. . . . . . . . 9 |- ( j e. A -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( n e. C |-> ( j ( j e. A , k e. C |-> X ) n ) ) )
66		nfcv 2593	. . . . . . . . . . 11 |- F/_ k j
67		nfmpt22 6347	. . . . . . . . . . 11 |- F/_ k ( j e. A , k e. C |-> X )
68		nfcv 2593	. . . . . . . . . . 11 |- F/_ k n
69	66, 67, 68	nfov 6302	. . . . . . . . . 10 |- F/_ k ( j ( j e. A , k e. C |-> X ) n )
70		nfcv 2593	. . . . . . . . . 10 |- F/_ n ( j ( j e. A , k e. C |-> X ) k )
71		oveq2 6284	. . . . . . . . . 10 |- ( n = k -> ( j ( j e. A , k e. C |-> X ) n ) = ( j ( j e. A , k e. C |-> X ) k ) )
72	69, 70, 71	cbvmpt 4466	. . . . . . . . 9 |- ( n e. C |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) )
73	65, 72	syl6eq 2502	. . . . . . . 8 |- ( j e. A -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) )
74	73	adantl 472	. . . . . . 7 |- ( ( ph /\ j e. A ) -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) )
75		simprl 769	. . . . . . . . . 10 |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> j e. A )
76		simprr 771	. . . . . . . . . 10 |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> k e. C )
77	33	ovmpt4g 6407	. . . . . . . . . 10 |- ( ( j e. A /\ k e. C /\ X e. B ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
78	75, 76, 31, 77	syl3anc 1271	. . . . . . . . 9 |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
79	78	anassrs 658	. . . . . . . 8 |- ( ( ( ph /\ j e. A ) /\ k e. C ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
80	79	mpteq2dva 4461	. . . . . . 7 |- ( ( ph /\ j e. A ) -> ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) = ( k e. C |-> X ) )
81	74, 80	eqtrd 2486	. . . . . 6 |- ( ( ph /\ j e. A ) -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> X ) )
82	81	oveq2d 6292	. . . . 5 |- ( ( ph /\ j e. A ) -> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) = ( G gsumg ( k e. C |-> X ) ) )
83	82	mpteq2dva 4461	. . . 4 |- ( ph -> ( j e. A |-> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsumg ( k e. C |-> X ) ) ) )
84	57, 83	syl5eq 2498	. . 3 |- ( ph -> ( m e. A |-> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsumg ( k e. C |-> X ) ) ) )
85	84	oveq2d 6292	. 2 |- ( ph -> ( G gsumg ( m e. A |-> ( G gsumg ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) ) = ( G gsumg ( j e. A |-> ( G gsumg ( k e. C |-> X ) ) ) ) )
86	39, 85	eqtrd 2486	1 |- ( ph -> ( G gsumg ( j e. A , k e. C |-> X ) ) = ( G gsumg ( j e. A |-> ( G gsumg ( k e. C |-> X ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 375   = wceq 1448   E.wex 1667   e. wcel 1891   A.wral 2737   _Vcvv 3013   {csn 3936   <.cop 3942   U_ciun 4248   class class class wbr 4374   |-> cmpt 4433   X. cxp 4810   dom cdm 4812   "cima 4815   Rel wrel 4817   -->wf 5557   ` cfv 5561  (class class class)co 6276   |-> cmpt2 6278   Fincfn 7556   Basecbs 15132   0gc0g 15349   gsum_g cgsu 15350  CMndccmn 17441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-inf2 8133  ax-cnex 9582  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-int 4205  df-iun 4250  df-iin 4251  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-se 4772  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-isom 5570  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-of 6519  df-om 6681  df-1st 6781  df-2nd 6782  df-supp 6903  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-fsupp 7871  df-oi 8012  df-card 8360  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-nn 10599  df-2 10657  df-n0 10860  df-z 10928  df-uz 11150  df-fz 11776  df-fzo 11909  df-seq 12208  df-hash 12510  df-ndx 15135  df-slot 15136  df-base 15137  df-sets 15138  df-ress 15139  df-plusg 15214  df-0g 15351  df-gsum 15352  df-mre 15503  df-mrc 15504  df-acs 15506  df-mgm 16499  df-sgrp 16538  df-mnd 16548  df-submnd 16594  df-mulg 16687  df-cntz 16982  df-cmn 17443

This theorem is referenced by:  gsumdixp  17848  psrass1lem  18612  gsumcom3  19435  gsummpt2co  28550