Metamath Proof Explorer

Theorem gsum2d

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)

Ref Expression
Hypotheses 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 gsum2d 
|- ( ph -> ( G gsum F ) = ( G gsum ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsum2d.b 
 |-  B = ( Base ` G )
2 gsum2d.z 
 |-  .0. = ( 0g ` G )
3 gsum2d.g 
 |-  ( ph -> G e. CMnd )
4 gsum2d.a 
 |-  ( ph -> A e. V )
5 gsum2d.r 
 |-  ( ph -> Rel A )
6 gsum2d.d 
 |-  ( ph -> D e. W )
7 gsum2d.s 
 |-  ( ph -> dom A C_ D )
8 gsum2d.f 
 |-  ( ph -> F : A --> B )
9 gsum2d.w 
 |-  ( ph -> F finSupp .0. )
10 1 2 3 4 5 6 7 8 9 gsum2dlem2 
 |-  ( ph -> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
11 suppssdm 
 |-  ( F supp .0. ) C_ dom F
12 11 8 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
13 relss 
 |-  ( ( F supp .0. ) C_ A -> ( Rel A -> Rel ( F supp .0. ) ) )
14 12 5 13 sylc 
 |-  ( ph -> Rel ( F supp .0. ) )
15 relssdmrn 
 |-  ( Rel ( F supp .0. ) -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) )
16 ssv 
 |-  ran ( F supp .0. ) C_ _V
17 xpss2 
 |-  ( ran ( F supp .0. ) C_ _V -> ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) C_ ( dom ( F supp .0. ) X. _V ) )
18 16 17 ax-mp 
 |-  ( dom ( F supp .0. ) X. ran ( F supp .0. ) ) C_ ( dom ( F supp .0. ) X. _V )
19 15 18 sstrdi 
 |-  ( Rel ( F supp .0. ) -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. _V ) )
20 14 19 syl 
 |-  ( ph -> ( F supp .0. ) C_ ( dom ( F supp .0. ) X. _V ) )
21 12 20 ssind 
 |-  ( ph -> ( F supp .0. ) C_ ( A i^i ( dom ( F supp .0. ) X. _V ) ) )
22 df-res 
 |-  ( A |` dom ( F supp .0. ) ) = ( A i^i ( dom ( F supp .0. ) X. _V ) )
23 21 22 sseqtrrdi 
 |-  ( ph -> ( F supp .0. ) C_ ( A |` dom ( F supp .0. ) ) )
24 1 2 3 4 8 23 9 gsumres 
 |-  ( ph -> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum F ) )
25 dmss 
 |-  ( ( F supp .0. ) C_ A -> dom ( F supp .0. ) C_ dom A )
26 12 25 syl 
 |-  ( ph -> dom ( F supp .0. ) C_ dom A )
27 26 7 sstrd 
 |-  ( ph -> dom ( F supp .0. ) C_ D )
28 27 resmptd 
 |-  ( ph -> ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) |` dom ( F supp .0. ) ) = ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
29 28 oveq2d 
 |-  ( ph -> ( G gsum ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) |` dom ( F supp .0. ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
30 1 2 3 4 5 6 7 8 9 gsum2dlem1 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
31 30 adantr 
 |-  ( ( ph /\ j e. D ) -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
32 31 fmpttd 
 |-  ( ph -> ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) : D --> B )
33 vex 
 |-  j e. _V
34 vex 
 |-  k e. _V
35 33 34 elimasn 
 |-  ( k e. ( A " { j } ) <-> <. j , k >. e. A )
36 35 biimpi 
 |-  ( k e. ( A " { j } ) -> <. j , k >. e. A )
37 36 ad2antll 
 |-  ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> <. j , k >. e. A )
38 eldifn 
 |-  ( j e. ( D \ dom ( F supp .0. ) ) -> -. j e. dom ( F supp .0. ) )
39 38 ad2antrl 
 |-  ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> -. j e. dom ( F supp .0. ) )
40 33 34 opeldm 
 |-  ( <. j , k >. e. ( F supp .0. ) -> j e. dom ( F supp .0. ) )
41 39 40 nsyl 
 |-  ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> -. <. j , k >. e. ( F supp .0. ) )
42 37 41 eldifd 
 |-  ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
43 df-ov 
 |-  ( j F k ) = ( F ` <. j , k >. )
44 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
45 2 fvexi 
 |-  .0. e. _V
46 45 a1i 
 |-  ( ph -> .0. e. _V )
47 8 44 4 46 suppssr 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
48 43 47 syl5eq 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
49 42 48 syldan 
 |-  ( ( ph /\ ( j e. ( D \ dom ( F supp .0. ) ) /\ k e. ( A " { j } ) ) ) -> ( j F k ) = .0. )
50 49 anassrs 
 |-  ( ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) /\ k e. ( A " { j } ) ) -> ( j F k ) = .0. )
51 50 mpteq2dva 
 |-  ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { j } ) |-> .0. ) )
52 51 oveq2d 
 |-  ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( k e. ( A " { j } ) |-> .0. ) ) )
53 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
54 3 53 syl 
 |-  ( ph -> G e. Mnd )
55 imaexg 
 |-  ( A e. V -> ( A " { j } ) e. _V )
56 4 55 syl 
 |-  ( ph -> ( A " { j } ) e. _V )
57 2 gsumz 
 |-  ( ( G e. Mnd /\ ( A " { j } ) e. _V ) -> ( G gsum ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
58 54 56 57 syl2anc 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
59 58 adantr 
 |-  ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsum ( k e. ( A " { j } ) |-> .0. ) ) = .0. )
60 52 59 eqtrd 
 |-  ( ( ph /\ j e. ( D \ dom ( F supp .0. ) ) ) -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = .0. )
61 60 6 suppss2 
 |-  ( ph -> ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) C_ dom ( F supp .0. ) )
62 funmpt 
 |-  Fun ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) )
63 62 a1i 
 |-  ( ph -> Fun ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
64 9 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
65 dmfi 
 |-  ( ( F supp .0. ) e. Fin -> dom ( F supp .0. ) e. Fin )
66 64 65 syl 
 |-  ( ph -> dom ( F supp .0. ) e. Fin )
67 66 61 ssfid 
 |-  ( ph -> ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin )
68 6 mptexd 
 |-  ( ph -> ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V )
69 isfsupp 
 |-  ( ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) e. _V /\ .0. e. _V ) -> ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. <-> ( Fun ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) /\ ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin ) ) )
70 68 46 69 syl2anc 
 |-  ( ph -> ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. <-> ( Fun ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) /\ ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) supp .0. ) e. Fin ) ) )
71 63 67 70 mpbir2and 
 |-  ( ph -> ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) finSupp .0. )
72 1 2 3 6 32 61 71 gsumres 
 |-  ( ph -> ( G gsum ( ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) |` dom ( F supp .0. ) ) ) = ( G gsum ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
73 29 72 eqtr3d 
 |-  ( ph -> ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
74 10 24 73 3eqtr3d 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )