Metamath Proof Explorer


Theorem esum2dlem

Description: Lemma for esum2d (finite case). (Contributed by Thierry Arnoux, 17-May-2020) (Proof shortened by AV, 17-Sep-2021)

Ref Expression
Hypotheses esum2d.0 _ k F
esum2d.1 z = j k F = C
esum2d.2 φ A V
esum2d.3 φ j A B W
esum2d.4 φ j A k B C 0 +∞
esum2dlem.e φ A Fin
Assertion esum2dlem φ * j A * k B C = * z j A j × B F

Proof

Step Hyp Ref Expression
1 esum2d.0 _ k F
2 esum2d.1 z = j k F = C
3 esum2d.2 φ A V
4 esum2d.3 φ j A B W
5 esum2d.4 φ j A k B C 0 +∞
6 esum2dlem.e φ A Fin
7 esumeq1 a = * j a * k B C = * j * k B C
8 nfv z a =
9 iuneq1 a = j a j × B = j j × B
10 8 9 esumeq1d a = * z j a j × B F = * z j j × B F
11 7 10 eqeq12d a = * j a * k B C = * z j a j × B F * j * k B C = * z j j × B F
12 esumeq1 a = b * j a * k B C = * j b * k B C
13 nfv z a = b
14 iuneq1 a = b j a j × B = j b j × B
15 13 14 esumeq1d a = b * z j a j × B F = * z j b j × B F
16 12 15 eqeq12d a = b * j a * k B C = * z j a j × B F * j b * k B C = * z j b j × B F
17 esumeq1 a = b l * j a * k B C = * j b l * k B C
18 nfv z a = b l
19 iuneq1 a = b l j a j × B = j b l j × B
20 18 19 esumeq1d a = b l * z j a j × B F = * z j b l j × B F
21 17 20 eqeq12d a = b l * j a * k B C = * z j a j × B F * j b l * k B C = * z j b l j × B F
22 esumeq1 a = A * j a * k B C = * j A * k B C
23 nfv z a = A
24 iuneq1 a = A j a j × B = j A j × B
25 23 24 esumeq1d a = A * z j a j × B F = * z j A j × B F
26 22 25 eqeq12d a = A * j a * k B C = * z j a j × B F * j A * k B C = * z j A j × B F
27 esumnul * z F = 0
28 0iun j j × B =
29 esumeq1 j j × B = * z j j × B F = * z F
30 28 29 ax-mp * z j j × B F = * z F
31 esumnul * j * k B C = 0
32 27 30 31 3eqtr4ri * j * k B C = * z j j × B F
33 32 a1i φ * j * k B C = * z j j × B F
34 simpr φ b A l A b * j b * k B C = * z j b j × B F * j b * k B C = * z j b j × B F
35 nfcsb1v _ j l / j B
36 nfcsb1v _ j l / j C
37 35 36 nfesum2 _ j * k l / j B l / j C
38 csbeq1a j = l B = l / j B
39 csbeq1a j = l C = l / j C
40 38 39 esumeq12d j = l * k B C = * k l / j B l / j C
41 40 adantl φ b A l A b j = l * k B C = * k l / j B l / j C
42 simprr φ b A l A b l A b
43 42 eldifad φ b A l A b l A
44 4 adantlr φ b A l A b j A B W
45 44 ralrimiva φ b A l A b j A B W
46 rspcsbela l A j A B W l / j B W
47 43 45 46 syl2anc φ b A l A b l / j B W
48 simpll φ b A l A b k l / j B φ
49 43 adantr φ b A l A b k l / j B l A
50 simpr φ b A l A b k l / j B k l / j B
51 5 ex φ j A k B C 0 +∞
52 51 sbcimdv φ [˙l / j]˙ j A k B [˙l / j]˙ C 0 +∞
53 sbcan [˙l / j]˙ j A k B [˙l / j]˙ j A [˙l / j]˙ k B
54 sbcel1v [˙l / j]˙ j A l A
55 sbcel2 [˙l / j]˙ k B k l / j B
56 54 55 anbi12i [˙l / j]˙ j A [˙l / j]˙ k B l A k l / j B
57 53 56 bitri [˙l / j]˙ j A k B l A k l / j B
58 vex l V
59 sbcel1g l V [˙l / j]˙ C 0 +∞ l / j C 0 +∞
60 58 59 ax-mp [˙l / j]˙ C 0 +∞ l / j C 0 +∞
61 52 57 60 3imtr3g φ l A k l / j B l / j C 0 +∞
62 61 imp φ l A k l / j B l / j C 0 +∞
63 48 49 50 62 syl12anc φ b A l A b k l / j B l / j C 0 +∞
64 63 ralrimiva φ b A l A b k l / j B l / j C 0 +∞
65 nfcv _ k l / j B
66 65 esumcl l / j B W k l / j B l / j C 0 +∞ * k l / j B l / j C 0 +∞
67 47 64 66 syl2anc φ b A l A b * k l / j B l / j C 0 +∞
68 37 41 42 67 esumsnf φ b A l A b * j l * k B C = * k l / j B l / j C
69 nfv k φ b A l A b
70 nfv j z = l k
71 36 nfeq2 j F = l / j C
72 70 71 nfim j z = l k F = l / j C
73 opeq1 j = l j k = l k
74 73 eqeq2d j = l z = j k z = l k
75 39 eqeq2d j = l F = C F = l / j C
76 74 75 imbi12d j = l z = j k F = C z = l k F = l / j C
77 72 76 2 chvarfv z = l k F = l / j C
78 vsnid j j
79 78 a1i φ j A k B j j
80 simpr φ j A k B k B
81 79 80 opelxpd φ j A k B j k j × B
82 xp2nd z j × B 2 nd z B
83 xp1st z j × B 1 st z j
84 fvex 1 st z V
85 84 elsn 1 st z j 1 st z = j
86 83 85 sylib z j × B 1 st z = j
87 eqop z j × B z = j k 1 st z = j 2 nd z = k
88 86 87 mpbirand z j × B z = j k 2 nd z = k
89 eqcom 2 nd z = k k = 2 nd z
90 88 89 bitrdi z j × B z = j k k = 2 nd z
91 90 ad2antlr φ j A z j × B k B z = j k k = 2 nd z
92 91 ralrimiva φ j A z j × B k B z = j k k = 2 nd z
93 reu6i 2 nd z B k B z = j k k = 2 nd z ∃! k B z = j k
94 82 92 93 syl2an2 φ j A z j × B ∃! k B z = j k
95 81 94 f1mptrn φ j A Fun k B j k -1
96 95 ex φ j A Fun k B j k -1
97 96 sbcimdv φ [˙l / j]˙ j A [˙l / j]˙ Fun k B j k -1
98 sbcfung l V [˙l / j]˙ Fun k B j k -1 Fun l / j k B j k -1
99 csbcnv l / j k B j k -1 = l / j k B j k -1
100 csbmpt12 l V l / j k B j k = k l / j B l / j j k
101 csbopg l V l / j j k = l / j j l / j k
102 csbvarg l V l / j j = l
103 csbconstg l V l / j k = k
104 102 103 opeq12d l V l / j j l / j k = l k
105 101 104 eqtrd l V l / j j k = l k
106 105 mpteq2dv l V k l / j B l / j j k = k l / j B l k
107 100 106 eqtrd l V l / j k B j k = k l / j B l k
108 107 cnveqd l V l / j k B j k -1 = k l / j B l k -1
109 99 108 eqtr3id l V l / j k B j k -1 = k l / j B l k -1
110 109 funeqd l V Fun l / j k B j k -1 Fun k l / j B l k -1
111 98 110 bitrd l V [˙l / j]˙ Fun k B j k -1 Fun k l / j B l k -1
112 58 111 ax-mp [˙l / j]˙ Fun k B j k -1 Fun k l / j B l k -1
113 97 54 112 3imtr3g φ l A Fun k l / j B l k -1
114 113 imp φ l A Fun k l / j B l k -1
115 43 114 syldan φ b A l A b Fun k l / j B l k -1
116 vsnid l l
117 116 a1i φ b A l A b k l / j B l l
118 117 50 opelxpd φ b A l A b k l / j B l k l × l / j B
119 1 69 65 77 47 115 63 118 esumc φ b A l A b * k l / j B l / j C = * z t | k l / j B t = l k F
120 nfab1 _ t t | k l / j B t = l k
121 nfcv _ t l × l / j B
122 opeq1 i = l i k = l k
123 122 eqeq2d i = l t = i k t = l k
124 123 rexbidv i = l k l / j B t = i k k l / j B t = l k
125 58 124 rexsn i l k l / j B t = i k k l / j B t = l k
126 elxp2 t l × l / j B i l k l / j B t = i k
127 abid t t | k l / j B t = l k k l / j B t = l k
128 125 126 127 3bitr4ri t t | k l / j B t = l k t l × l / j B
129 120 121 128 eqri t | k l / j B t = l k = l × l / j B
130 esumeq1 t | k l / j B t = l k = l × l / j B * z t | k l / j B t = l k F = * z l × l / j B F
131 129 130 ax-mp * z t | k l / j B t = l k F = * z l × l / j B F
132 119 131 eqtrdi φ b A l A b * k l / j B l / j C = * z l × l / j B F
133 68 132 eqtrd φ b A l A b * j l * k B C = * z l × l / j B F
134 133 adantr φ b A l A b * j b * k B C = * z j b j × B F * j l * k B C = * z l × l / j B F
135 34 134 oveq12d φ b A l A b * j b * k B C = * z j b j × B F * j b * k B C + 𝑒 * j l * k B C = * z j b j × B F + 𝑒 * z l × l / j B F
136 nfv j φ b A l A b
137 nfcv _ j b
138 nfcv _ j l
139 vex b V
140 139 a1i φ b A l A b b V
141 snex l V
142 141 a1i φ b A l A b l V
143 42 eldifbd φ b A l A b ¬ l b
144 disjsn b l = ¬ l b
145 143 144 sylibr φ b A l A b b l =
146 simpll φ b A l A b j b φ
147 simprl φ b A l A b b A
148 147 sselda φ b A l A b j b j A
149 5 anassrs φ j A k B C 0 +∞
150 149 ralrimiva φ j A k B C 0 +∞
151 nfcv _ k B
152 151 esumcl B W k B C 0 +∞ * k B C 0 +∞
153 4 150 152 syl2anc φ j A * k B C 0 +∞
154 146 148 153 syl2anc φ b A l A b j b * k B C 0 +∞
155 simpll φ b A l A b j l φ
156 43 snssd φ b A l A b l A
157 156 sselda φ b A l A b j l j A
158 155 157 153 syl2anc φ b A l A b j l * k B C 0 +∞
159 136 137 138 140 142 145 154 158 esumsplit φ b A l A b * j b l * k B C = * j b * k B C + 𝑒 * j l * k B C
160 159 adantr φ b A l A b * j b * k B C = * z j b j × B F * j b l * k B C = * j b * k B C + 𝑒 * j l * k B C
161 iunxun j b l j × B = j b j × B j l j × B
162 138 35 nfxp _ j l × l / j B
163 sneq j = l j = l
164 163 38 xpeq12d j = l j × B = l × l / j B
165 162 164 iunxsngf l V j l j × B = l × l / j B
166 58 165 ax-mp j l j × B = l × l / j B
167 166 uneq2i j b j × B j l j × B = j b j × B l × l / j B
168 161 167 eqtri j b l j × B = j b j × B l × l / j B
169 esumeq1 j b l j × B = j b j × B l × l / j B * z j b l j × B F = * z j b j × B l × l / j B F
170 168 169 ax-mp * z j b l j × B F = * z j b j × B l × l / j B F
171 nfv z φ b A l A b
172 nfcv _ z j b j × B
173 nfcv _ z l × l / j B
174 snex j V
175 148 44 syldan φ b A l A b j b B W
176 xpexg j V B W j × B V
177 174 175 176 sylancr φ b A l A b j b j × B V
178 177 ralrimiva φ b A l A b j b j × B V
179 iunexg b V j b j × B V j b j × B V
180 139 178 179 sylancr φ b A l A b j b j × B V
181 xpexg l V l / j B W l × l / j B V
182 141 47 181 sylancr φ b A l A b l × l / j B V
183 simpr φ b A l A b j b j b
184 143 adantr φ b A l A b j b ¬ l b
185 nelne2 j b ¬ l b j l
186 183 184 185 syl2anc φ b A l A b j b j l
187 disjsn2 j l j l =
188 xpdisj1 j l = j × B l × l / j B =
189 186 187 188 3syl φ b A l A b j b j × B l × l / j B =
190 189 iuneq2dv φ b A l A b j b j × B l × l / j B = j b
191 162 iunin1f j b j × B l × l / j B = j b j × B l × l / j B
192 iun0 j b =
193 190 191 192 3eqtr3g φ b A l A b j b j × B l × l / j B =
194 simpll φ b A l A b z j b j × B φ
195 iunss1 b A j b j × B j A j × B
196 147 195 syl φ b A l A b j b j × B j A j × B
197 196 sselda φ b A l A b z j b j × B z j A j × B
198 nfv j φ
199 nfiu1 _ j j A j × B
200 199 nfcri j z j A j × B
201 198 200 nfan j φ z j A j × B
202 nfv k φ z j A j × B j A z j × B
203 nfcv _ k 0 +∞
204 1 203 nfel k F 0 +∞
205 2 adantl φ z j A j × B j A z j × B k B z = j k F = C
206 simp-5l φ z j A j × B j A z j × B k B z = j k φ
207 simp-4r φ z j A j × B j A z j × B k B z = j k j A
208 simplr φ z j A j × B j A z j × B k B z = j k k B
209 206 207 208 5 syl12anc φ z j A j × B j A z j × B k B z = j k C 0 +∞
210 205 209 eqeltrd φ z j A j × B j A z j × B k B z = j k F 0 +∞
211 elsnxp j A z j × B k B z = j k
212 211 biimpa j A z j × B k B z = j k
213 212 adantll φ z j A j × B j A z j × B k B z = j k
214 202 204 210 213 r19.29af2 φ z j A j × B j A z j × B F 0 +∞
215 simpr φ z j A j × B z j A j × B
216 eliun z j A j × B j A z j × B
217 215 216 sylib φ z j A j × B j A z j × B
218 201 214 217 r19.29af φ z j A j × B F 0 +∞
219 194 197 218 syl2anc φ b A l A b z j b j × B F 0 +∞
220 simpll φ b A l A b z l × l / j B φ
221 nfcv _ j A
222 nfcv _ j l
223 221 222 162 164 ssiun2sf l A l × l / j B j A j × B
224 43 223 syl φ b A l A b l × l / j B j A j × B
225 224 sselda φ b A l A b z l × l / j B z j A j × B
226 220 225 218 syl2anc φ b A l A b z l × l / j B F 0 +∞
227 171 172 173 180 182 193 219 226 esumsplit φ b A l A b * z j b j × B l × l / j B F = * z j b j × B F + 𝑒 * z l × l / j B F
228 170 227 syl5eq φ b A l A b * z j b l j × B F = * z j b j × B F + 𝑒 * z l × l / j B F
229 228 adantr φ b A l A b * j b * k B C = * z j b j × B F * z j b l j × B F = * z j b j × B F + 𝑒 * z l × l / j B F
230 135 160 229 3eqtr4d φ b A l A b * j b * k B C = * z j b j × B F * j b l * k B C = * z j b l j × B F
231 230 ex φ b A l A b * j b * k B C = * z j b j × B F * j b l * k B C = * z j b l j × B F
232 11 16 21 26 33 231 6 findcard2d φ * j A * k B C = * z j A j × B F