Metamath Proof Explorer

Theorem gsummpt2d

Description: Express a finite sum over a two-dimensional range as a double sum. See also gsum2d . (Contributed by Thierry Arnoux, 27-Apr-2020)

Ref Expression
Hypotheses gsummpt2d.c 
|- F/_ z C
gsummpt2d.0 
|- F/ y ph
gsummpt2d.b 
|- B = ( Base ` W )
gsummpt2d.1 
|- ( x = <. y , z >. -> C = D )
gsummpt2d.r 
|- ( ph -> Rel A )
gsummpt2d.2 
|- ( ph -> A e. Fin )
gsummpt2d.m 
|- ( ph -> W e. CMnd )
gsummpt2d.3 
|- ( ( ph /\ x e. A ) -> C e. B )
Assertion gsummpt2d 
|- ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( y e. dom A |-> ( W gsum ( z e. ( A " { y } ) |-> D ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummpt2d.c 
 |-  F/_ z C
2 gsummpt2d.0 
 |-  F/ y ph
3 gsummpt2d.b 
 |-  B = ( Base ` W )
4 gsummpt2d.1 
 |-  ( x = <. y , z >. -> C = D )
5 gsummpt2d.r 
 |-  ( ph -> Rel A )
6 gsummpt2d.2 
 |-  ( ph -> A e. Fin )
7 gsummpt2d.m 
 |-  ( ph -> W e. CMnd )
8 gsummpt2d.3 
 |-  ( ( ph /\ x e. A ) -> C e. B )
9 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
10 6 dmexd 
 |-  ( ph -> dom A e. _V )
11 1stdm 
 |-  ( ( Rel A /\ x e. A ) -> ( 1st ` x ) e. dom A )
12 5 11 sylan 
 |-  ( ( ph /\ x e. A ) -> ( 1st ` x ) e. dom A )
13 fo1st 
 |-  1st : _V -onto-> _V
14 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
15 dffn5 
 |-  ( 1st Fn _V <-> 1st = ( x e. _V |-> ( 1st ` x ) ) )
16 15 biimpi 
 |-  ( 1st Fn _V -> 1st = ( x e. _V |-> ( 1st ` x ) ) )
17 13 14 16 mp2b 
 |-  1st = ( x e. _V |-> ( 1st ` x ) )
18 17 reseq1i 
 |-  ( 1st |` A ) = ( ( x e. _V |-> ( 1st ` x ) ) |` A )
19 ssv 
 |-  A C_ _V
20 resmpt 
 |-  ( A C_ _V -> ( ( x e. _V |-> ( 1st ` x ) ) |` A ) = ( x e. A |-> ( 1st ` x ) ) )
21 19 20 ax-mp 
 |-  ( ( x e. _V |-> ( 1st ` x ) ) |` A ) = ( x e. A |-> ( 1st ` x ) )
22 18 21 eqtri 
 |-  ( 1st |` A ) = ( x e. A |-> ( 1st ` x ) )
23 3 9 7 6 10 8 12 22 gsummpt2co 
 |-  ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( y e. dom A |-> ( W gsum ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) ) ) ) )
24 7 adantr 
 |-  ( ( ph /\ y e. dom A ) -> W e. CMnd )
25 6 adantr 
 |-  ( ( ph /\ y e. dom A ) -> A e. Fin )
26 imaexg 
 |-  ( A e. Fin -> ( A " { y } ) e. _V )
27 25 26 syl 
 |-  ( ( ph /\ y e. dom A ) -> ( A " { y } ) e. _V )
28 4 adantl 
 |-  ( ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x e. A ) /\ x = <. y , z >. ) -> C = D )
29 simp-4l 
 |-  ( ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x e. A ) /\ x = <. y , z >. ) -> ph )
30 simplr 
 |-  ( ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x e. A ) /\ x = <. y , z >. ) -> x e. A )
31 29 30 8 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x e. A ) /\ x = <. y , z >. ) -> C e. B )
32 28 31 eqeltrrd 
 |-  ( ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x e. A ) /\ x = <. y , z >. ) -> D e. B )
33 vex 
 |-  y e. _V
34 vex 
 |-  z e. _V
35 33 34 elimasn 
 |-  ( z e. ( A " { y } ) <-> <. y , z >. e. A )
36 35 biimpi 
 |-  ( z e. ( A " { y } ) -> <. y , z >. e. A )
37 36 adantl 
 |-  ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) -> <. y , z >. e. A )
38 simpr 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x = <. y , z >. ) -> x = <. y , z >. )
39 38 eqeq1d 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) /\ x = <. y , z >. ) -> ( x = <. y , z >. <-> <. y , z >. = <. y , z >. ) )
40 eqidd 
 |-  ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) -> <. y , z >. = <. y , z >. )
41 37 39 40 rspcedvd 
 |-  ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) -> E. x e. A x = <. y , z >. )
42 32 41 r19.29a 
 |-  ( ( ( ph /\ y e. dom A ) /\ z e. ( A " { y } ) ) -> D e. B )
43 42 fmpttd 
 |-  ( ( ph /\ y e. dom A ) -> ( z e. ( A " { y } ) |-> D ) : ( A " { y } ) --> B )
44 eqid 
 |-  ( z e. ( A " { y } ) |-> D ) = ( z e. ( A " { y } ) |-> D )
45 imafi2 
 |-  ( A e. Fin -> ( A " { y } ) e. Fin )
46 6 45 syl 
 |-  ( ph -> ( A " { y } ) e. Fin )
47 46 adantr 
 |-  ( ( ph /\ y e. dom A ) -> ( A " { y } ) e. Fin )
48 fvex 
 |-  ( 0g ` W ) e. _V
49 48 a1i 
 |-  ( ( ph /\ y e. dom A ) -> ( 0g ` W ) e. _V )
50 44 47 42 49 fsuppmptdm 
 |-  ( ( ph /\ y e. dom A ) -> ( z e. ( A " { y } ) |-> D ) finSupp ( 0g ` W ) )
51 2ndconst 
 |-  ( y e. dom A -> ( 2nd |` ( { y } X. ( A " { y } ) ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) )
52 51 adantl 
 |-  ( ( ph /\ y e. dom A ) -> ( 2nd |` ( { y } X. ( A " { y } ) ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) )
53 1stpreimas 
 |-  ( ( Rel A /\ y e. dom A ) -> ( `' ( 1st |` A ) " { y } ) = ( { y } X. ( A " { y } ) ) )
54 5 53 sylan 
 |-  ( ( ph /\ y e. dom A ) -> ( `' ( 1st |` A ) " { y } ) = ( { y } X. ( A " { y } ) ) )
55 54 reseq2d 
 |-  ( ( ph /\ y e. dom A ) -> ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) = ( 2nd |` ( { y } X. ( A " { y } ) ) ) )
56 f1oeq1 
 |-  ( ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) = ( 2nd |` ( { y } X. ( A " { y } ) ) ) -> ( ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) <-> ( 2nd |` ( { y } X. ( A " { y } ) ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) ) )
57 55 56 syl 
 |-  ( ( ph /\ y e. dom A ) -> ( ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) <-> ( 2nd |` ( { y } X. ( A " { y } ) ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) ) )
58 52 57 mpbird 
 |-  ( ( ph /\ y e. dom A ) -> ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) : ( { y } X. ( A " { y } ) ) -1-1-onto-> ( A " { y } ) )
59 3 9 24 27 43 50 58 gsumf1o 
 |-  ( ( ph /\ y e. dom A ) -> ( W gsum ( z e. ( A " { y } ) |-> D ) ) = ( W gsum ( ( z e. ( A " { y } ) |-> D ) o. ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) ) ) )
60 simpr 
 |-  ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) -> x e. ( `' ( 1st |` A ) " { y } ) )
61 54 adantr 
 |-  ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) -> ( `' ( 1st |` A ) " { y } ) = ( { y } X. ( A " { y } ) ) )
62 60 61 eleqtrd 
 |-  ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) -> x e. ( { y } X. ( A " { y } ) ) )
63 xp2nd 
 |-  ( x e. ( { y } X. ( A " { y } ) ) -> ( 2nd ` x ) e. ( A " { y } ) )
64 62 63 syl 
 |-  ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) -> ( 2nd ` x ) e. ( A " { y } ) )
65 64 ralrimiva 
 |-  ( ( ph /\ y e. dom A ) -> A. x e. ( `' ( 1st |` A ) " { y } ) ( 2nd ` x ) e. ( A " { y } ) )
66 fo2nd 
 |-  2nd : _V -onto-> _V
67 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
68 dffn5 
 |-  ( 2nd Fn _V <-> 2nd = ( x e. _V |-> ( 2nd ` x ) ) )
69 68 biimpi 
 |-  ( 2nd Fn _V -> 2nd = ( x e. _V |-> ( 2nd ` x ) ) )
70 66 67 69 mp2b 
 |-  2nd = ( x e. _V |-> ( 2nd ` x ) )
71 70 reseq1i 
 |-  ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) = ( ( x e. _V |-> ( 2nd ` x ) ) |` ( `' ( 1st |` A ) " { y } ) )
72 ssv 
 |-  ( `' ( 1st |` A ) " { y } ) C_ _V
73 resmpt 
 |-  ( ( `' ( 1st |` A ) " { y } ) C_ _V -> ( ( x e. _V |-> ( 2nd ` x ) ) |` ( `' ( 1st |` A ) " { y } ) ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> ( 2nd ` x ) ) )
74 72 73 ax-mp 
 |-  ( ( x e. _V |-> ( 2nd ` x ) ) |` ( `' ( 1st |` A ) " { y } ) ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> ( 2nd ` x ) )
75 71 74 eqtri 
 |-  ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> ( 2nd ` x ) )
76 75 a1i 
 |-  ( ( ph /\ y e. dom A ) -> ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> ( 2nd ` x ) ) )
77 eqidd 
 |-  ( ( ph /\ y e. dom A ) -> ( z e. ( A " { y } ) |-> D ) = ( z e. ( A " { y } ) |-> D ) )
78 65 76 77 fmptcos 
 |-  ( ( ph /\ y e. dom A ) -> ( ( z e. ( A " { y } ) |-> D ) o. ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> [_ ( 2nd ` x ) / z ]_ D ) )
79 nfv 
 |-  F/ z ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) )
80 1 a1i 
 |-  ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) -> F/_ z C )
81 62 adantr 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> x e. ( { y } X. ( A " { y } ) ) )
82 xp1st 
 |-  ( x e. ( { y } X. ( A " { y } ) ) -> ( 1st ` x ) e. { y } )
83 81 82 syl 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> ( 1st ` x ) e. { y } )
84 fvex 
 |-  ( 1st ` x ) e. _V
85 84 elsn 
 |-  ( ( 1st ` x ) e. { y } <-> ( 1st ` x ) = y )
86 83 85 sylib 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> ( 1st ` x ) = y )
87 simpr 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> z = ( 2nd ` x ) )
88 87 eqcomd 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> ( 2nd ` x ) = z )
89 eqopi 
 |-  ( ( x e. ( { y } X. ( A " { y } ) ) /\ ( ( 1st ` x ) = y /\ ( 2nd ` x ) = z ) ) -> x = <. y , z >. )
90 81 86 88 89 syl12anc 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> x = <. y , z >. )
91 90 4 syl 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> C = D )
92 91 eqcomd 
 |-  ( ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) /\ z = ( 2nd ` x ) ) -> D = C )
93 79 80 64 92 csbiedf 
 |-  ( ( ( ph /\ y e. dom A ) /\ x e. ( `' ( 1st |` A ) " { y } ) ) -> [_ ( 2nd ` x ) / z ]_ D = C )
94 93 mpteq2dva 
 |-  ( ( ph /\ y e. dom A ) -> ( x e. ( `' ( 1st |` A ) " { y } ) |-> [_ ( 2nd ` x ) / z ]_ D ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) )
95 78 94 eqtrd 
 |-  ( ( ph /\ y e. dom A ) -> ( ( z e. ( A " { y } ) |-> D ) o. ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) ) = ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) )
96 95 oveq2d 
 |-  ( ( ph /\ y e. dom A ) -> ( W gsum ( ( z e. ( A " { y } ) |-> D ) o. ( 2nd |` ( `' ( 1st |` A ) " { y } ) ) ) ) = ( W gsum ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) ) )
97 59 96 eqtr2d 
 |-  ( ( ph /\ y e. dom A ) -> ( W gsum ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) ) = ( W gsum ( z e. ( A " { y } ) |-> D ) ) )
98 2 97 mpteq2da 
 |-  ( ph -> ( y e. dom A |-> ( W gsum ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) ) ) = ( y e. dom A |-> ( W gsum ( z e. ( A " { y } ) |-> D ) ) ) )
99 98 oveq2d 
 |-  ( ph -> ( W gsum ( y e. dom A |-> ( W gsum ( x e. ( `' ( 1st |` A ) " { y } ) |-> C ) ) ) ) = ( W gsum ( y e. dom A |-> ( W gsum ( z e. ( A " { y } ) |-> D ) ) ) ) )
100 23 99 eqtrd 
 |-  ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( y e. dom A |-> ( W gsum ( z e. ( A " { y } ) |-> D ) ) ) ) )