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 x φ
gsumfs2d.b B = Base W
gsumfs2d.1 0 ˙ = 0 W
gsumfs2d.r φ Rel A
gsumfs2d.2 φ finSupp 0 ˙ F
gsumfs2d.w φ W CMnd
gsumfs2d.3 φ F : A B
gsumfs2d.a φ A X
Assertion gsumfs2d φ W F = W x dom A W y A x F x y

Proof

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