Metamath Proof Explorer

Theorem gsumfs2d

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses gsumfs2d.p 
|- F/ x ph
gsumfs2d.b 
|- B = ( Base ` W )
gsumfs2d.1 
|- .0. = ( 0g ` W )
gsumfs2d.r 
|- ( ph -> Rel A )
gsumfs2d.2 
|- ( ph -> F finSupp .0. )
gsumfs2d.w 
|- ( ph -> W e. CMnd )
gsumfs2d.3 
|- ( ph -> F : A --> B )
gsumfs2d.a 
|- ( ph -> A e. X )
Assertion gsumfs2d 
|- ( ph -> ( W gsum F ) = ( W gsum ( x e. dom A |-> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumfs2d.p 
 |-  F/ x ph
2 gsumfs2d.b 
 |-  B = ( Base ` W )
3 gsumfs2d.1 
 |-  .0. = ( 0g ` W )
4 gsumfs2d.r 
 |-  ( ph -> Rel A )
5 gsumfs2d.2 
 |-  ( ph -> F finSupp .0. )
6 gsumfs2d.w 
 |-  ( ph -> W e. CMnd )
7 gsumfs2d.3 
 |-  ( ph -> F : A --> B )
8 gsumfs2d.a 
 |-  ( ph -> A e. X )
9 6 adantr 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> W e. CMnd )
10 8 adantr 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> A e. X )
11 10 imaexd 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> ( A " { x } ) e. _V )
12 7 ffnd 
 |-  ( ph -> F Fn A )
13 12 ad2antrr 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> F Fn A )
14 8 ad2antrr 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> A e. X )
15 3 fvexi 
 |-  .0. e. _V
16 15 a1i 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> .0. e. _V )
17 simpr 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) )
18 17 eldifad 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> y e. ( A " { x } ) )
19 vex 
 |-  x e. _V
20 vex 
 |-  y e. _V
21 19 20 elimasn 
 |-  ( y e. ( A " { x } ) <-> <. x , y >. e. A )
22 21 biimpi 
 |-  ( y e. ( A " { x } ) -> <. x , y >. e. A )
23 18 22 syl 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> <. x , y >. e. A )
24 17 eldifbd 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> -. y e. ( ( F supp .0. ) " { x } ) )
25 19 20 elimasn 
 |-  ( y e. ( ( F supp .0. ) " { x } ) <-> <. x , y >. e. ( F supp .0. ) )
26 25 biimpri 
 |-  ( <. x , y >. e. ( F supp .0. ) -> y e. ( ( F supp .0. ) " { x } ) )
27 24 26 nsyl 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> -. <. x , y >. e. ( F supp .0. ) )
28 23 27 eldifd 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> <. x , y >. e. ( A \ ( F supp .0. ) ) )
29 13 14 16 28 fvdifsupp 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( ( A " { x } ) \ ( ( F supp .0. ) " { x } ) ) ) -> ( F ` <. x , y >. ) = .0. )
30 5 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
31 30 adantr 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> ( F supp .0. ) e. Fin )
32 imafi2 
 |-  ( ( F supp .0. ) e. Fin -> ( ( F supp .0. ) " { x } ) e. Fin )
33 31 32 syl 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> ( ( F supp .0. ) " { x } ) e. Fin )
34 7 ad2antrr 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( A " { x } ) ) -> F : A --> B )
35 22 adantl 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( A " { x } ) ) -> <. x , y >. e. A )
36 34 35 ffvelcdmd 
 |-  ( ( ( ph /\ x e. dom ( F supp .0. ) ) /\ y e. ( A " { x } ) ) -> ( F ` <. x , y >. ) e. B )
37 suppssdm 
 |-  ( F supp .0. ) C_ dom F
38 37 7 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
39 38 adantr 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> ( F supp .0. ) C_ A )
40 imass1 
 |-  ( ( F supp .0. ) C_ A -> ( ( F supp .0. ) " { x } ) C_ ( A " { x } ) )
41 39 40 syl 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> ( ( F supp .0. ) " { x } ) C_ ( A " { x } ) )
42 2 3 9 11 29 33 36 41 gsummptres2 
 |-  ( ( ph /\ x e. dom ( F supp .0. ) ) -> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) = ( W gsum ( y e. ( ( F supp .0. ) " { x } ) |-> ( F ` <. x , y >. ) ) ) )
43 42 mpteq2dva 
 |-  ( ph -> ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) ) = ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( ( F supp .0. ) " { x } ) |-> ( F ` <. x , y >. ) ) ) ) )
44 43 oveq2d 
 |-  ( ph -> ( W gsum ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) = ( W gsum ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( ( F supp .0. ) " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) )
45 8 dmexd 
 |-  ( ph -> dom A e. _V )
46 12 ad2antrr 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> F Fn A )
47 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> A e. X )
48 15 a1i 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> .0. e. _V )
49 22 adantl 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> <. x , y >. e. A )
50 simplr 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> x e. ( dom A \ dom ( F supp .0. ) ) )
51 50 eldifbd 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> -. x e. dom ( F supp .0. ) )
52 19 20 opeldm 
 |-  ( <. x , y >. e. ( F supp .0. ) -> x e. dom ( F supp .0. ) )
53 51 52 nsyl 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> -. <. x , y >. e. ( F supp .0. ) )
54 49 53 eldifd 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> <. x , y >. e. ( A \ ( F supp .0. ) ) )
55 46 47 48 54 fvdifsupp 
 |-  ( ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) /\ y e. ( A " { x } ) ) -> ( F ` <. x , y >. ) = .0. )
56 55 mpteq2dva 
 |-  ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) -> ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) = ( y e. ( A " { x } ) |-> .0. ) )
57 56 oveq2d 
 |-  ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) -> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) = ( W gsum ( y e. ( A " { x } ) |-> .0. ) ) )
58 6 cmnmndd 
 |-  ( ph -> W e. Mnd )
59 8 adantr 
 |-  ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) -> A e. X )
60 59 imaexd 
 |-  ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) -> ( A " { x } ) e. _V )
61 3 gsumz 
 |-  ( ( W e. Mnd /\ ( A " { x } ) e. _V ) -> ( W gsum ( y e. ( A " { x } ) |-> .0. ) ) = .0. )
62 58 60 61 syl2an2r 
 |-  ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) -> ( W gsum ( y e. ( A " { x } ) |-> .0. ) ) = .0. )
63 57 62 eqtrd 
 |-  ( ( ph /\ x e. ( dom A \ dom ( F supp .0. ) ) ) -> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) = .0. )
64 dmfi 
 |-  ( ( F supp .0. ) e. Fin -> dom ( F supp .0. ) e. Fin )
65 30 64 syl 
 |-  ( ph -> dom ( F supp .0. ) e. Fin )
66 6 adantr 
 |-  ( ( ph /\ x e. dom A ) -> W e. CMnd )
67 8 adantr 
 |-  ( ( ph /\ x e. dom A ) -> A e. X )
68 67 imaexd 
 |-  ( ( ph /\ x e. dom A ) -> ( A " { x } ) e. _V )
69 7 ad2antrr 
 |-  ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) -> F : A --> B )
70 22 adantl 
 |-  ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) -> <. x , y >. e. A )
71 69 70 ffvelcdmd 
 |-  ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) -> ( F ` <. x , y >. ) e. B )
72 71 fmpttd 
 |-  ( ( ph /\ x e. dom A ) -> ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) : ( A " { x } ) --> B )
73 68 mptexd 
 |-  ( ( ph /\ x e. dom A ) -> ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) e. _V )
74 72 ffnd 
 |-  ( ( ph /\ x e. dom A ) -> ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) Fn ( A " { x } ) )
75 15 a1i 
 |-  ( ( ph /\ x e. dom A ) -> .0. e. _V )
76 30 adantr 
 |-  ( ( ph /\ x e. dom A ) -> ( F supp .0. ) e. Fin )
77 76 32 syl 
 |-  ( ( ph /\ x e. dom A ) -> ( ( F supp .0. ) " { x } ) e. Fin )
78 eqid 
 |-  ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) = ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) )
79 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> ph )
80 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> x e. dom A )
81 simpr 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> y = t )
82 simpllr 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> t e. ( A " { x } ) )
83 81 82 eqeltrd 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> y e. ( A " { x } ) )
84 simplr 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> -. t e. ( ( F supp .0. ) " { x } ) )
85 81 84 eqneltrd 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> -. y e. ( ( F supp .0. ) " { x } ) )
86 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> F Fn A )
87 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> A e. X )
88 15 a1i 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> .0. e. _V )
89 70 adantr 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> <. x , y >. e. A )
90 26 con3i 
 |-  ( -. y e. ( ( F supp .0. ) " { x } ) -> -. <. x , y >. e. ( F supp .0. ) )
91 90 adantl 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> -. <. x , y >. e. ( F supp .0. ) )
92 89 91 eldifd 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> <. x , y >. e. ( A \ ( F supp .0. ) ) )
93 86 87 88 92 fvdifsupp 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ y e. ( A " { x } ) ) /\ -. y e. ( ( F supp .0. ) " { x } ) ) -> ( F ` <. x , y >. ) = .0. )
94 79 80 83 85 93 syl1111anc 
 |-  ( ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) /\ y = t ) -> ( F ` <. x , y >. ) = .0. )
95 simplr 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) -> t e. ( A " { x } ) )
96 15 a1i 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) -> .0. e. _V )
97 78 94 95 96 fvmptd2 
 |-  ( ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) /\ -. t e. ( ( F supp .0. ) " { x } ) ) -> ( ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ` t ) = .0. )
98 97 ex 
 |-  ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) -> ( -. t e. ( ( F supp .0. ) " { x } ) -> ( ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ` t ) = .0. ) )
99 98 orrd 
 |-  ( ( ( ph /\ x e. dom A ) /\ t e. ( A " { x } ) ) -> ( t e. ( ( F supp .0. ) " { x } ) \/ ( ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ` t ) = .0. ) )
100 73 74 75 77 99 finnzfsuppd 
 |-  ( ( ph /\ x e. dom A ) -> ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) finSupp .0. )
101 2 3 66 68 72 100 gsumcl 
 |-  ( ( ph /\ x e. dom A ) -> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) e. B )
102 dmss 
 |-  ( ( F supp .0. ) C_ A -> dom ( F supp .0. ) C_ dom A )
103 38 102 syl 
 |-  ( ph -> dom ( F supp .0. ) C_ dom A )
104 2 3 6 45 63 65 101 103 gsummptres2 
 |-  ( ph -> ( W gsum ( x e. dom A |-> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) = ( W gsum ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) )
105 7 38 feqresmpt 
 |-  ( ph -> ( F |` ( F supp .0. ) ) = ( z e. ( F supp .0. ) |-> ( F ` z ) ) )
106 105 oveq2d 
 |-  ( ph -> ( W gsum ( F |` ( F supp .0. ) ) ) = ( W gsum ( z e. ( F supp .0. ) |-> ( F ` z ) ) ) )
107 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
108 2 3 6 8 7 107 5 gsumres 
 |-  ( ph -> ( W gsum ( F |` ( F supp .0. ) ) ) = ( W gsum F ) )
109 nfcv 
 |-  F/_ y ( F ` z )
110 fveq2 
 |-  ( z = <. x , y >. -> ( F ` z ) = ( F ` <. x , y >. ) )
111 relss 
 |-  ( ( F supp .0. ) C_ A -> ( Rel A -> Rel ( F supp .0. ) ) )
112 38 4 111 sylc 
 |-  ( ph -> Rel ( F supp .0. ) )
113 7 adantr 
 |-  ( ( ph /\ z e. ( F supp .0. ) ) -> F : A --> B )
114 38 sselda 
 |-  ( ( ph /\ z e. ( F supp .0. ) ) -> z e. A )
115 113 114 ffvelcdmd 
 |-  ( ( ph /\ z e. ( F supp .0. ) ) -> ( F ` z ) e. B )
116 109 1 2 110 112 30 6 115 gsummpt2d 
 |-  ( ph -> ( W gsum ( z e. ( F supp .0. ) |-> ( F ` z ) ) ) = ( W gsum ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( ( F supp .0. ) " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) )
117 106 108 116 3eqtr3d 
 |-  ( ph -> ( W gsum F ) = ( W gsum ( x e. dom ( F supp .0. ) |-> ( W gsum ( y e. ( ( F supp .0. ) " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) )
118 44 104 117 3eqtr4rd 
 |-  ( ph -> ( W gsum F ) = ( W gsum ( x e. dom A |-> ( W gsum ( y e. ( A " { x } ) |-> ( F ` <. x , y >. ) ) ) ) ) )