MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsum2d Structured version   Unicode version

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
StepHypRef 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.  )
101, 2, 3, 4, 5, 6, 7, 8, 9gsum2dlem2 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 )
138, 12syl 16 . . . . . 6  |-  ( ph  ->  dom  F  =  A )
1411, 13syl5sseq 3394 . . . . 5  |-  ( ph  ->  ( F supp  .0.  )  C_  A )
15 relss 4916 . . . . . . 7  |-  ( ( F supp  .0.  )  C_  A  ->  ( Rel  A  ->  Rel  ( F supp  .0.  ) ) )
1614, 5, 15sylc 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 ) )
2018, 19ax-mp 5 . . . . . . 7  |-  ( dom  ( F supp  .0.  )  X.  ran  ( F supp  .0.  ) )  C_  ( dom  ( F supp  .0.  )  X.  _V )
2117, 20syl6ss 3358 . . . . . 6  |-  ( Rel  ( F supp  .0.  )  ->  ( F supp  .0.  )  C_  ( dom  ( F supp 
.0.  )  X.  _V ) )
2216, 21syl 16 . . . . 5  |-  ( ph  ->  ( F supp  .0.  )  C_  ( dom  ( F supp 
.0.  )  X.  _V ) )
2314, 22ssind 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 ) )
2523, 24syl6sseqr 3393 . . 3  |-  ( ph  ->  ( F supp  .0.  )  C_  ( A  |`  dom  ( F supp  .0.  ) ) )
261, 2, 3, 4, 8, 25, 9gsumres 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 )
2814, 27syl 16 . . . . . 6  |-  ( ph  ->  dom  ( F supp  .0.  )  C_  dom  A )
2928, 7sstrd 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 ) ) ) ) )
3129, 30syl 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 ) ) ) ) )
3231oveq2d 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 ) ) ) ) ) )
331, 2, 3, 4, 5, 6, 7, 8, 9gsum2dlem1 16437 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( k  e.  ( A " { j } )  |->  ( j F k ) ) )  e.  B )
3433adantr 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 ) ) ) )
3634, 35fmptd 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
3937, 38elimasn 5184 . . . . . . . . . . . . 13  |-  ( k  e.  ( A " { j } )  <->  <. j ,  k >.  e.  A )
4039biimpi 194 . . . . . . . . . . . 12  |-  ( k  e.  ( A " { j } )  ->  <. j ,  k
>.  e.  A )
4140ad2antll 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.  ) )
4342ad2antrl 722 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( j  e.  ( D  \  dom  ( F supp  .0.  ) )  /\  k  e.  ( A " { j } ) ) )  ->  -.  j  e.  dom  ( F supp  .0.  )
)
4437, 38opeldm 5032 . . . . . . . . . . . 12  |-  ( <.
j ,  k >.  e.  ( F supp  .0.  )  ->  j  e.  dom  ( F supp  .0.  ) )
4543, 44nsyl 121 . . . . . . . . . . 11  |-  ( (
ph  /\  ( j  e.  ( D  \  dom  ( F supp  .0.  ) )  /\  k  e.  ( A " { j } ) ) )  ->  -.  <. j ,  k >.  e.  ( F supp  .0.  ) )
4641, 45eldifd 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.  )
4948a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( F supp  .0.  )  C_  ( F supp  .0.  )
)
50 fvex 5691 . . . . . . . . . . . . . 14  |-  ( 0g
`  G )  e. 
_V
512, 50eqeltri 2505 . . . . . . . . . . . . 13  |-  .0.  e.  _V
5251a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  .0.  e.  _V )
538, 49, 4, 52suppssr 6711 . . . . . . . . . . 11  |-  ( (
ph  /\  <. j ,  k >.  e.  ( A  \  ( F supp  .0.  ) ) )  -> 
( F `  <. j ,  k >. )  =  .0.  )
5447, 53syl5eq 2479 . . . . . . . . . 10  |-  ( (
ph  /\  <. j ,  k >.  e.  ( A  \  ( F supp  .0.  ) ) )  -> 
( j F k )  =  .0.  )
5546, 54syldan 467 . . . . . . . . 9  |-  ( (
ph  /\  ( j  e.  ( D  \  dom  ( F supp  .0.  ) )  /\  k  e.  ( A " { j } ) ) )  ->  ( j F k )  =  .0.  )
5655anassrs 643 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( D  \  dom  ( F supp  .0.  ) ) )  /\  k  e.  ( A " {
j } ) )  ->  ( j F k )  =  .0.  )
5756mpteq2dva 4368 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( D  \  dom  ( F supp  .0.  ) ) )  ->  ( k  e.  ( A " {
j } )  |->  ( j F k ) )  =  ( k  e.  ( A " { j } ) 
|->  .0.  ) )
5857oveq2d 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 )
603, 59syl 16 . . . . . . . 8  |-  ( ph  ->  G  e.  Mnd )
61 imaexg 6506 . . . . . . . . 9  |-  ( A  e.  V  ->  ( A " { j } )  e.  _V )
624, 61syl 16 . . . . . . . 8  |-  ( ph  ->  ( A " {
j } )  e. 
_V )
632gsumz 15493 . . . . . . . 8  |-  ( ( G  e.  Mnd  /\  ( A " { j } )  e.  _V )  ->  ( G  gsumg  ( k  e.  ( A " { j } ) 
|->  .0.  ) )  =  .0.  )
6460, 62, 63syl2anc 656 . . . . . . 7  |-  ( ph  ->  ( G  gsumg  ( k  e.  ( A " { j } )  |->  .0.  )
)  =  .0.  )
6564adantr 462 . . . . . 6  |-  ( (
ph  /\  j  e.  ( D  \  dom  ( F supp  .0.  ) ) )  ->  ( G  gsumg  ( k  e.  ( A " { j } ) 
|->  .0.  ) )  =  .0.  )
6658, 65eqtrd 2467 . . . . 5  |-  ( (
ph  /\  j  e.  ( D  \  dom  ( F supp  .0.  ) ) )  ->  ( G  gsumg  ( k  e.  ( A " { j } ) 
|->  ( j F k ) ) )  =  .0.  )
6766, 6suppss2 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 ) ) ) )
6968a1i 11 . . . . 5  |-  ( ph  ->  Fun  ( j  e.  D  |->  ( G  gsumg  ( k  e.  ( A " { j } ) 
|->  ( j F k ) ) ) ) )
709fsuppimpd 7617 . . . . . . 7  |-  ( ph  ->  ( F supp  .0.  )  e.  Fin )
71 dmfi 7584 . . . . . . 7  |-  ( ( F supp  .0.  )  e.  Fin  ->  dom  ( F supp  .0.  )  e.  Fin )
7270, 71syl 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 )
7472, 67, 73syl2anc 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 )
766, 75syl 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 ) ) )
7876, 52, 77syl2anc 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 ) ) )
7969, 74, 78mpbir2and 908 . . . 4  |-  ( ph  ->  ( j  e.  D  |->  ( G  gsumg  ( k  e.  ( A " { j } )  |->  ( j F k ) ) ) ) finSupp  .0.  )
801, 2, 3, 6, 36, 67, 79gsumres 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 ) ) ) ) ) )
8132, 80eqtr3d 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 ) ) ) ) ) )
8210, 26, 813eqtr3d 2475 1  |-  ( ph  ->  ( G  gsumg  F )  =  ( G  gsumg  ( j  e.  D  |->  ( G  gsumg  ( k  e.  ( A " { j } )  |->  ( j F k ) ) ) ) ) )
Colors of variables: wff setvar class
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    gsumg 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
  Copyright terms: Public domain W3C validator