Metamath Proof Explorer


Theorem dvnprodlem3

Description: The multinomial formula for the k -th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnprodlem3.s φ S
dvnprodlem3.x φ X TopOpen fld 𝑡 S
dvnprodlem3.t φ T Fin
dvnprodlem3.h φ t T H t : X
dvnprodlem3.n φ N 0
dvnprodlem3.dvnh φ t T j 0 N S D n H t j : X
dvnprodlem3.f F = x X t T H t x
dvnprodlem3.d D = s 𝒫 T n 0 c 0 n s | t s c t = n
dvnprodlem3.c C = n 0 c 0 n T | t T c t = n
Assertion dvnprodlem3 φ S D n F N = x X c C N N ! t T c t ! t T S D n H t c t x

Proof

Step Hyp Ref Expression
1 dvnprodlem3.s φ S
2 dvnprodlem3.x φ X TopOpen fld 𝑡 S
3 dvnprodlem3.t φ T Fin
4 dvnprodlem3.h φ t T H t : X
5 dvnprodlem3.n φ N 0
6 dvnprodlem3.dvnh φ t T j 0 N S D n H t j : X
7 dvnprodlem3.f F = x X t T H t x
8 dvnprodlem3.d D = s 𝒫 T n 0 c 0 n s | t s c t = n
9 dvnprodlem3.c C = n 0 c 0 n T | t T c t = n
10 prodeq1 s = t s H t x = t H t x
11 10 mpteq2dv s = x X t s H t x = x X t H t x
12 11 oveq2d s = S D n x X t s H t x = S D n x X t H t x
13 12 fveq1d s = S D n x X t s H t x k = S D n x X t H t x k
14 fveq2 s = D s = D
15 14 fveq1d s = D s k = D k
16 15 sumeq1d s = c D s k k ! t s c t ! t s S D n H t c t x = c D k k ! t s c t ! t s S D n H t c t x
17 prodeq1 s = t s c t ! = t c t !
18 17 oveq2d s = k ! t s c t ! = k ! t c t !
19 prodeq1 s = t s S D n H t c t x = t S D n H t c t x
20 18 19 oveq12d s = k ! t s c t ! t s S D n H t c t x = k ! t c t ! t S D n H t c t x
21 20 sumeq2sdv s = c D k k ! t s c t ! t s S D n H t c t x = c D k k ! t c t ! t S D n H t c t x
22 16 21 eqtrd s = c D s k k ! t s c t ! t s S D n H t c t x = c D k k ! t c t ! t S D n H t c t x
23 22 mpteq2dv s = x X c D s k k ! t s c t ! t s S D n H t c t x = x X c D k k ! t c t ! t S D n H t c t x
24 13 23 eqeq12d s = S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
25 24 ralbidv s = k 0 N S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x k 0 N S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
26 prodeq1 s = r t s H t x = t r H t x
27 26 mpteq2dv s = r x X t s H t x = x X t r H t x
28 27 oveq2d s = r S D n x X t s H t x = S D n x X t r H t x
29 28 fveq1d s = r S D n x X t s H t x k = S D n x X t r H t x k
30 fveq2 s = r D s = D r
31 30 fveq1d s = r D s k = D r k
32 31 sumeq1d s = r c D s k k ! t s c t ! t s S D n H t c t x = c D r k k ! t s c t ! t s S D n H t c t x
33 prodeq1 s = r t s c t ! = t r c t !
34 33 oveq2d s = r k ! t s c t ! = k ! t r c t !
35 prodeq1 s = r t s S D n H t c t x = t r S D n H t c t x
36 34 35 oveq12d s = r k ! t s c t ! t s S D n H t c t x = k ! t r c t ! t r S D n H t c t x
37 36 sumeq2sdv s = r c D r k k ! t s c t ! t s S D n H t c t x = c D r k k ! t r c t ! t r S D n H t c t x
38 32 37 eqtrd s = r c D s k k ! t s c t ! t s S D n H t c t x = c D r k k ! t r c t ! t r S D n H t c t x
39 38 mpteq2dv s = r x X c D s k k ! t s c t ! t s S D n H t c t x = x X c D r k k ! t r c t ! t r S D n H t c t x
40 29 39 eqeq12d s = r S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x
41 40 ralbidv s = r k 0 N S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x
42 prodeq1 s = r z t s H t x = t r z H t x
43 42 mpteq2dv s = r z x X t s H t x = x X t r z H t x
44 43 oveq2d s = r z S D n x X t s H t x = S D n x X t r z H t x
45 44 fveq1d s = r z S D n x X t s H t x k = S D n x X t r z H t x k
46 fveq2 s = r z D s = D r z
47 46 fveq1d s = r z D s k = D r z k
48 47 sumeq1d s = r z c D s k k ! t s c t ! t s S D n H t c t x = c D r z k k ! t s c t ! t s S D n H t c t x
49 prodeq1 s = r z t s c t ! = t r z c t !
50 49 oveq2d s = r z k ! t s c t ! = k ! t r z c t !
51 prodeq1 s = r z t s S D n H t c t x = t r z S D n H t c t x
52 50 51 oveq12d s = r z k ! t s c t ! t s S D n H t c t x = k ! t r z c t ! t r z S D n H t c t x
53 52 sumeq2sdv s = r z c D r z k k ! t s c t ! t s S D n H t c t x = c D r z k k ! t r z c t ! t r z S D n H t c t x
54 48 53 eqtrd s = r z c D s k k ! t s c t ! t s S D n H t c t x = c D r z k k ! t r z c t ! t r z S D n H t c t x
55 54 mpteq2dv s = r z x X c D s k k ! t s c t ! t s S D n H t c t x = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
56 45 55 eqeq12d s = r z S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x S D n x X t r z H t x k = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
57 56 ralbidv s = r z k 0 N S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x k 0 N S D n x X t r z H t x k = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
58 prodeq1 s = T t s H t x = t T H t x
59 58 mpteq2dv s = T x X t s H t x = x X t T H t x
60 7 a1i s = T F = x X t T H t x
61 60 eqcomd s = T x X t T H t x = F
62 59 61 eqtrd s = T x X t s H t x = F
63 62 oveq2d s = T S D n x X t s H t x = S D n F
64 63 fveq1d s = T S D n x X t s H t x k = S D n F k
65 fveq2 s = T D s = D T
66 65 fveq1d s = T D s k = D T k
67 66 sumeq1d s = T c D s k k ! t s c t ! t s S D n H t c t x = c D T k k ! t s c t ! t s S D n H t c t x
68 prodeq1 s = T t s c t ! = t T c t !
69 68 oveq2d s = T k ! t s c t ! = k ! t T c t !
70 prodeq1 s = T t s S D n H t c t x = t T S D n H t c t x
71 69 70 oveq12d s = T k ! t s c t ! t s S D n H t c t x = k ! t T c t ! t T S D n H t c t x
72 71 sumeq2sdv s = T c D T k k ! t s c t ! t s S D n H t c t x = c D T k k ! t T c t ! t T S D n H t c t x
73 67 72 eqtrd s = T c D s k k ! t s c t ! t s S D n H t c t x = c D T k k ! t T c t ! t T S D n H t c t x
74 73 mpteq2dv s = T x X c D s k k ! t s c t ! t s S D n H t c t x = x X c D T k k ! t T c t ! t T S D n H t c t x
75 64 74 eqeq12d s = T S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x S D n F k = x X c D T k k ! t T c t ! t T S D n H t c t x
76 75 ralbidv s = T k 0 N S D n x X t s H t x k = x X c D s k k ! t s c t ! t s S D n H t c t x k 0 N S D n F k = x X c D T k k ! t T c t ! t T S D n H t c t x
77 prod0 t H t x = 1
78 77 mpteq2i x X t H t x = x X 1
79 78 oveq2i S D n x X t H t x = S D n x X 1
80 79 a1i k = 0 S D n x X t H t x = S D n x X 1
81 id k = 0 k = 0
82 80 81 fveq12d k = 0 S D n x X t H t x k = S D n x X 1 0
83 82 adantl φ k = 0 S D n x X t H t x k = S D n x X 1 0
84 recnprss S S
85 1 84 syl φ S
86 1cnd φ x X 1
87 86 fmpttd φ x X 1 : X
88 1re 1
89 88 rgenw x X 1
90 dmmptg x X 1 dom x X 1 = X
91 89 90 ax-mp dom x X 1 = X
92 91 a1i φ dom x X 1 = X
93 92 feq2d φ x X 1 : dom x X 1 x X 1 : X
94 87 93 mpbird φ x X 1 : dom x X 1
95 restsspw TopOpen fld 𝑡 S 𝒫 S
96 95 2 sseldi φ X 𝒫 S
97 elpwi X 𝒫 S X S
98 96 97 syl φ X S
99 92 98 eqsstrd φ dom x X 1 S
100 94 99 jca φ x X 1 : dom x X 1 dom x X 1 S
101 cnex V
102 101 a1i φ V
103 elpm2g V S x X 1 𝑝𝑚 S x X 1 : dom x X 1 dom x X 1 S
104 102 1 103 syl2anc φ x X 1 𝑝𝑚 S x X 1 : dom x X 1 dom x X 1 S
105 100 104 mpbird φ x X 1 𝑝𝑚 S
106 dvn0 S x X 1 𝑝𝑚 S S D n x X 1 0 = x X 1
107 85 105 106 syl2anc φ S D n x X 1 0 = x X 1
108 107 adantr φ k = 0 S D n x X 1 0 = x X 1
109 fveq2 k = 0 D k = D 0
110 109 adantl φ k = 0 D k = D 0
111 oveq2 s = 0 n s = 0 n
112 elmapfn x 0 n x Fn
113 fn0 x Fn x =
114 112 113 sylib x 0 n x =
115 velsn x x =
116 114 115 sylibr x 0 n x
117 115 biimpi x x =
118 id x = x =
119 f0 : 0 n
120 ovex 0 n V
121 0ex V
122 120 121 elmap 0 n : 0 n
123 119 122 mpbir 0 n
124 123 a1i x = 0 n
125 118 124 eqeltrd x = x 0 n
126 117 125 syl x x 0 n
127 116 126 impbii x 0 n x
128 127 ax-gen x x 0 n x
129 dfcleq 0 n = x x 0 n x
130 128 129 mpbir 0 n =
131 130 a1i s = 0 n =
132 111 131 eqtrd s = 0 n s =
133 rabeq 0 n s = c 0 n s | t s c t = n = c | t s c t = n
134 132 133 syl s = c 0 n s | t s c t = n = c | t s c t = n
135 sumeq1 s = t s c t = t c t
136 135 eqeq1d s = t s c t = n t c t = n
137 136 rabbidv s = c | t s c t = n = c | t c t = n
138 134 137 eqtrd s = c 0 n s | t s c t = n = c | t c t = n
139 138 mpteq2dv s = n 0 c 0 n s | t s c t = n = n 0 c | t c t = n
140 0elpw 𝒫 T
141 140 a1i φ 𝒫 T
142 nn0ex 0 V
143 142 mptex n 0 c | t c t = n V
144 143 a1i φ n 0 c | t c t = n V
145 8 139 141 144 fvmptd3 φ D = n 0 c | t c t = n
146 eqeq2 n = 0 t c t = n t c t = 0
147 146 rabbidv n = 0 c | t c t = n = c | t c t = 0
148 147 adantl φ n = 0 c | t c t = n = c | t c t = 0
149 0nn0 0 0
150 149 a1i φ 0 0
151 p0ex V
152 151 rabex c | t c t = 0 V
153 152 a1i φ c | t c t = 0 V
154 145 148 150 153 fvmptd φ D 0 = c | t c t = 0
155 154 adantr φ k = 0 D 0 = c | t c t = 0
156 snidg V
157 121 156 ax-mp
158 eqid 0 = 0
159 157 158 pm3.2i 0 = 0
160 sum0 t c t = 0
161 160 a1i c = t c t = 0
162 161 eqeq1d c = t c t = 0 0 = 0
163 162 elrab c | t c t = 0 0 = 0
164 159 163 mpbir c | t c t = 0
165 164 n0ii ¬ c | t c t = 0 =
166 eqid c | t c t = 0 = c | t c t = 0
167 rabrsn c | t c t = 0 = c | t c t = 0 c | t c t = 0 = c | t c t = 0 =
168 166 167 ax-mp c | t c t = 0 = c | t c t = 0 =
169 165 168 mtpor c | t c t = 0 =
170 169 a1i φ k = 0 c | t c t = 0 =
171 iftrue k = 0 if k = 0 =
172 171 adantl φ k = 0 if k = 0 =
173 170 172 eqtr4d φ k = 0 c | t c t = 0 = if k = 0
174 110 155 173 3eqtrd φ k = 0 D k = if k = 0
175 174 172 eqtrd φ k = 0 D k =
176 175 sumeq1d φ k = 0 c D k k ! t c t ! t S D n H t c t x = c k ! t c t ! t S D n H t c t x
177 fveq2 k = 0 k ! = 0 !
178 fac0 0 ! = 1
179 178 a1i k = 0 0 ! = 1
180 177 179 eqtrd k = 0 k ! = 1
181 180 oveq1d k = 0 k ! t c t ! = 1 t c t !
182 prod0 t c t ! = 1
183 182 oveq2i 1 t c t ! = 1 1
184 1div1e1 1 1 = 1
185 183 184 eqtri 1 t c t ! = 1
186 181 185 eqtrdi k = 0 k ! t c t ! = 1
187 prod0 t S D n H t c t x = 1
188 187 a1i k = 0 t S D n H t c t x = 1
189 186 188 oveq12d k = 0 k ! t c t ! t S D n H t c t x = 1 1
190 189 ad2antlr φ k = 0 c k ! t c t ! t S D n H t c t x = 1 1
191 1t1e1 1 1 = 1
192 191 a1i φ k = 0 c 1 1 = 1
193 190 192 eqtrd φ k = 0 c k ! t c t ! t S D n H t c t x = 1
194 193 sumeq2dv φ k = 0 c k ! t c t ! t S D n H t c t x = c 1
195 ax-1cn 1
196 eqidd c = 1 = 1
197 196 sumsn V 1 c 1 = 1
198 121 195 197 mp2an c 1 = 1
199 198 a1i φ k = 0 c 1 = 1
200 176 194 199 3eqtrd φ k = 0 c D k k ! t c t ! t S D n H t c t x = 1
201 200 mpteq2dv φ k = 0 x X c D k k ! t c t ! t S D n H t c t x = x X 1
202 201 eqcomd φ k = 0 x X 1 = x X c D k k ! t c t ! t S D n H t c t x
203 83 108 202 3eqtrd φ k = 0 S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
204 203 a1d φ k = 0 k 0 N S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
205 79 fveq1i S D n x X t H t x k = S D n x X 1 k
206 205 a1i φ ¬ k = 0 k 0 N S D n x X t H t x k = S D n x X 1 k
207 1 adantr φ ¬ k = 0 S
208 207 adantr φ ¬ k = 0 k 0 N S
209 2 adantr φ ¬ k = 0 X TopOpen fld 𝑡 S
210 209 adantr φ ¬ k = 0 k 0 N X TopOpen fld 𝑡 S
211 195 a1i φ ¬ k = 0 k 0 N 1
212 elfznn0 k 0 N k 0
213 212 adantl ¬ k = 0 k 0 N k 0
214 neqne ¬ k = 0 k 0
215 214 adantr ¬ k = 0 k 0 N k 0
216 213 215 jca ¬ k = 0 k 0 N k 0 k 0
217 elnnne0 k k 0 k 0
218 216 217 sylibr ¬ k = 0 k 0 N k
219 218 adantll φ ¬ k = 0 k 0 N k
220 208 210 211 219 dvnmptconst φ ¬ k = 0 k 0 N S D n x X 1 k = x X 0
221 145 ad2antrr φ ¬ k = 0 k 0 N D = n 0 c | t c t = n
222 eqeq2 n = k t c t = n t c t = k
223 222 rabbidv n = k c | t c t = n = c | t c t = k
224 223 adantl ¬ k = 0 n = k c | t c t = n = c | t c t = k
225 eqidd t c t = k k = k
226 id t c t = k t c t = k
227 226 eqcomd t c t = k k = t c t
228 160 a1i t c t = k t c t = 0
229 225 227 228 3eqtrd t c t = k k = 0
230 229 adantl c t c t = k k = 0
231 230 adantll ¬ k = 0 c t c t = k k = 0
232 simpll ¬ k = 0 c t c t = k ¬ k = 0
233 231 232 pm2.65da ¬ k = 0 c ¬ t c t = k
234 233 ralrimiva ¬ k = 0 c ¬ t c t = k
235 rabeq0 c | t c t = k = c ¬ t c t = k
236 234 235 sylibr ¬ k = 0 c | t c t = k =
237 236 adantr ¬ k = 0 n = k c | t c t = k =
238 224 237 eqtrd ¬ k = 0 n = k c | t c t = n =
239 238 adantll φ ¬ k = 0 n = k c | t c t = n =
240 239 adantlr φ ¬ k = 0 k 0 N n = k c | t c t = n =
241 212 adantl φ ¬ k = 0 k 0 N k 0
242 121 a1i φ ¬ k = 0 k 0 N V
243 221 240 241 242 fvmptd φ ¬ k = 0 k 0 N D k =
244 243 sumeq1d φ ¬ k = 0 k 0 N c D k k ! t c t ! t S D n H t c t x = c k ! t c t ! t S D n H t c t x
245 sum0 c k ! t c t ! t S D n H t c t x = 0
246 245 a1i φ ¬ k = 0 k 0 N c k ! t c t ! t S D n H t c t x = 0
247 244 246 eqtr2d φ ¬ k = 0 k 0 N 0 = c D k k ! t c t ! t S D n H t c t x
248 247 mpteq2dv φ ¬ k = 0 k 0 N x X 0 = x X c D k k ! t c t ! t S D n H t c t x
249 206 220 248 3eqtrd φ ¬ k = 0 k 0 N S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
250 249 ex φ ¬ k = 0 k 0 N S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
251 204 250 pm2.61dan φ k 0 N S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
252 251 ralrimiv φ k 0 N S D n x X t H t x k = x X c D k k ! t c t ! t S D n H t c t x
253 simpll φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x j 0 N φ r T z T r
254 fveq2 x = y H t x = H t y
255 254 prodeq2ad x = y t r H t x = t r H t y
256 fveq2 t = u H t = H u
257 256 fveq1d t = u H t y = H u y
258 257 cbvprodv t r H t y = u r H u y
259 258 a1i x = y t r H t y = u r H u y
260 255 259 eqtrd x = y t r H t x = u r H u y
261 260 cbvmptv x X t r H t x = y X u r H u y
262 261 oveq2i S D n x X t r H t x = S D n y X u r H u y
263 262 fveq1i S D n x X t r H t x k = S D n y X u r H u y k
264 fveq2 t = u c t = c u
265 264 fveq2d t = u c t ! = c u !
266 265 cbvprodv t r c t ! = u r c u !
267 266 oveq2i k ! t r c t ! = k ! u r c u !
268 267 a1i x = y k ! t r c t ! = k ! u r c u !
269 fveq2 x = y S D n H t c t x = S D n H t c t y
270 269 prodeq2ad x = y t r S D n H t c t x = t r S D n H t c t y
271 256 oveq2d t = u S D n H t = S D n H u
272 271 264 fveq12d t = u S D n H t c t = S D n H u c u
273 272 fveq1d t = u S D n H t c t y = S D n H u c u y
274 273 cbvprodv t r S D n H t c t y = u r S D n H u c u y
275 274 a1i x = y t r S D n H t c t y = u r S D n H u c u y
276 270 275 eqtrd x = y t r S D n H t c t x = u r S D n H u c u y
277 268 276 oveq12d x = y k ! t r c t ! t r S D n H t c t x = k ! u r c u ! u r S D n H u c u y
278 277 sumeq2sdv x = y c D r k k ! t r c t ! t r S D n H t c t x = c D r k k ! u r c u ! u r S D n H u c u y
279 fveq1 c = d c u = d u
280 279 fveq2d c = d c u ! = d u !
281 280 prodeq2ad c = d u r c u ! = u r d u !
282 281 oveq2d c = d k ! u r c u ! = k ! u r d u !
283 279 fveq2d c = d S D n H u c u = S D n H u d u
284 283 fveq1d c = d S D n H u c u y = S D n H u d u y
285 284 prodeq2ad c = d u r S D n H u c u y = u r S D n H u d u y
286 282 285 oveq12d c = d k ! u r c u ! u r S D n H u c u y = k ! u r d u ! u r S D n H u d u y
287 286 cbvsumv c D r k k ! u r c u ! u r S D n H u c u y = d D r k k ! u r d u ! u r S D n H u d u y
288 287 a1i x = y c D r k k ! u r c u ! u r S D n H u c u y = d D r k k ! u r d u ! u r S D n H u d u y
289 278 288 eqtrd x = y c D r k k ! t r c t ! t r S D n H t c t x = d D r k k ! u r d u ! u r S D n H u d u y
290 289 cbvmptv x X c D r k k ! t r c t ! t r S D n H t c t x = y X d D r k k ! u r d u ! u r S D n H u d u y
291 263 290 eqeq12i S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y
292 291 ralbii k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y
293 292 biimpi k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y
294 293 ad2antlr φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x j 0 N k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y
295 simpr φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x j 0 N j 0 N
296 1 ad3antrrr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N S
297 2 ad3antrrr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N X TopOpen fld 𝑡 S
298 3 ad3antrrr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N T Fin
299 simp-4l φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T φ
300 simpr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T t T
301 299 300 4 syl2anc φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T H t : X
302 5 ad3antrrr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N N 0
303 simplll φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N φ
304 303 3ad2ant1 φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T h 0 N φ
305 simp2 φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T h 0 N t T
306 simp3 φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T h 0 N h 0 N
307 eleq1w j = h j 0 N h 0 N
308 307 3anbi3d j = h φ t T j 0 N φ t T h 0 N
309 fveq2 j = h S D n H t j = S D n H t h
310 309 feq1d j = h S D n H t j : X S D n H t h : X
311 308 310 imbi12d j = h φ t T j 0 N S D n H t j : X φ t T h 0 N S D n H t h : X
312 311 6 chvarvv φ t T h 0 N S D n H t h : X
313 304 305 306 312 syl3anc φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N t T h 0 N S D n H t h : X
314 simprl φ r T z T r r T
315 314 ad2antrr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N r T
316 simprr φ r T z T r z T r
317 316 ad2antrr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N z T r
318 262 eqcomi S D n y X u r H u y = S D n x X t r H t x
319 318 a1i k = l S D n y X u r H u y = S D n x X t r H t x
320 id k = l k = l
321 319 320 fveq12d k = l S D n y X u r H u y k = S D n x X t r H t x l
322 290 eqcomi y X d D r k k ! u r d u ! u r S D n H u d u y = x X c D r k k ! t r c t ! t r S D n H t c t x
323 322 a1i k = l y X d D r k k ! u r d u ! u r S D n H u d u y = x X c D r k k ! t r c t ! t r S D n H t c t x
324 fveq2 k = l k ! = l !
325 324 oveq1d k = l k ! t r c t ! = l ! t r c t !
326 325 oveq1d k = l k ! t r c t ! t r S D n H t c t x = l ! t r c t ! t r S D n H t c t x
327 326 sumeq2sdv k = l c D r k k ! t r c t ! t r S D n H t c t x = c D r k l ! t r c t ! t r S D n H t c t x
328 fveq2 k = l D r k = D r l
329 328 sumeq1d k = l c D r k l ! t r c t ! t r S D n H t c t x = c D r l l ! t r c t ! t r S D n H t c t x
330 327 329 eqtrd k = l c D r k k ! t r c t ! t r S D n H t c t x = c D r l l ! t r c t ! t r S D n H t c t x
331 330 mpteq2dv k = l x X c D r k k ! t r c t ! t r S D n H t c t x = x X c D r l l ! t r c t ! t r S D n H t c t x
332 323 331 eqtrd k = l y X d D r k k ! u r d u ! u r S D n H u d u y = x X c D r l l ! t r c t ! t r S D n H t c t x
333 321 332 eqeq12d k = l S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y S D n x X t r H t x l = x X c D r l l ! t r c t ! t r S D n H t c t x
334 333 cbvralvw k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y l 0 N S D n x X t r H t x l = x X c D r l l ! t r c t ! t r S D n H t c t x
335 334 biimpi k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y l 0 N S D n x X t r H t x l = x X c D r l l ! t r c t ! t r S D n H t c t x
336 335 ad2antlr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N l 0 N S D n x X t r H t x l = x X c D r l l ! t r c t ! t r S D n H t c t x
337 simpr φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N j 0 N
338 fveq1 d = c d z = c z
339 338 oveq2d d = c j d z = j c z
340 reseq1 d = c d r = c r
341 339 340 opeq12d d = c j d z d r = j c z c r
342 341 cbvmptv d D r z j j d z d r = c D r z j j c z c r
343 296 297 298 301 302 313 8 315 317 336 337 342 dvnprodlem2 φ r T z T r k 0 N S D n y X u r H u y k = y X d D r k k ! u r d u ! u r S D n H u d u y j 0 N S D n x X t r z H t x j = x X c D r z j j ! t r z c t ! t r z S D n H t c t x
344 253 294 295 343 syl21anc φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x j 0 N S D n x X t r z H t x j = x X c D r z j j ! t r z c t ! t r z S D n H t c t x
345 344 ralrimiva φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x j 0 N S D n x X t r z H t x j = x X c D r z j j ! t r z c t ! t r z S D n H t c t x
346 fveq2 j = k S D n x X t r z H t x j = S D n x X t r z H t x k
347 fveq2 j = k j ! = k !
348 347 oveq1d j = k j ! t r z c t ! = k ! t r z c t !
349 348 oveq1d j = k j ! t r z c t ! t r z S D n H t c t x = k ! t r z c t ! t r z S D n H t c t x
350 349 sumeq2sdv j = k c D r z j j ! t r z c t ! t r z S D n H t c t x = c D r z j k ! t r z c t ! t r z S D n H t c t x
351 fveq2 j = k D r z j = D r z k
352 351 sumeq1d j = k c D r z j k ! t r z c t ! t r z S D n H t c t x = c D r z k k ! t r z c t ! t r z S D n H t c t x
353 350 352 eqtrd j = k c D r z j j ! t r z c t ! t r z S D n H t c t x = c D r z k k ! t r z c t ! t r z S D n H t c t x
354 353 mpteq2dv j = k x X c D r z j j ! t r z c t ! t r z S D n H t c t x = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
355 346 354 eqeq12d j = k S D n x X t r z H t x j = x X c D r z j j ! t r z c t ! t r z S D n H t c t x S D n x X t r z H t x k = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
356 355 cbvralvw j 0 N S D n x X t r z H t x j = x X c D r z j j ! t r z c t ! t r z S D n H t c t x k 0 N S D n x X t r z H t x k = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
357 345 356 sylib φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x k 0 N S D n x X t r z H t x k = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
358 357 ex φ r T z T r k 0 N S D n x X t r H t x k = x X c D r k k ! t r c t ! t r S D n H t c t x k 0 N S D n x X t r z H t x k = x X c D r z k k ! t r z c t ! t r z S D n H t c t x
359 25 41 57 76 252 358 3 findcard2d φ k 0 N S D n F k = x X c D T k k ! t T c t ! t T S D n H t c t x
360 nn0uz 0 = 0
361 5 360 eleqtrdi φ N 0
362 eluzfz2 N 0 N 0 N
363 361 362 syl φ N 0 N
364 fveq2 k = N S D n F k = S D n F N
365 fveq2 k = N D T k = D T N
366 365 sumeq1d k = N c D T k k ! t T c t ! t T S D n H t c t x = c D T N k ! t T c t ! t T S D n H t c t x
367 fveq2 k = N k ! = N !
368 367 oveq1d k = N k ! t T c t ! = N ! t T c t !
369 368 oveq1d k = N k ! t T c t ! t T S D n H t c t x = N ! t T c t ! t T S D n H t c t x
370 369 sumeq2sdv k = N c D T N k ! t T c t ! t T S D n H t c t x = c D T N N ! t T c t ! t T S D n H t c t x
371 366 370 eqtrd k = N c D T k k ! t T c t ! t T S D n H t c t x = c D T N N ! t T c t ! t T S D n H t c t x
372 371 mpteq2dv k = N x X c D T k k ! t T c t ! t T S D n H t c t x = x X c D T N N ! t T c t ! t T S D n H t c t x
373 364 372 eqeq12d k = N S D n F k = x X c D T k k ! t T c t ! t T S D n H t c t x S D n F N = x X c D T N N ! t T c t ! t T S D n H t c t x
374 373 rspccva k 0 N S D n F k = x X c D T k k ! t T c t ! t T S D n H t c t x N 0 N S D n F N = x X c D T N N ! t T c t ! t T S D n H t c t x
375 359 363 374 syl2anc φ S D n F N = x X c D T N N ! t T c t ! t T S D n H t c t x
376 oveq2 s = T 0 n s = 0 n T
377 rabeq 0 n s = 0 n T c 0 n s | t s c t = n = c 0 n T | t s c t = n
378 376 377 syl s = T c 0 n s | t s c t = n = c 0 n T | t s c t = n
379 sumeq1 s = T t s c t = t T c t
380 379 eqeq1d s = T t s c t = n t T c t = n
381 380 rabbidv s = T c 0 n T | t s c t = n = c 0 n T | t T c t = n
382 378 381 eqtrd s = T c 0 n s | t s c t = n = c 0 n T | t T c t = n
383 382 mpteq2dv s = T n 0 c 0 n s | t s c t = n = n 0 c 0 n T | t T c t = n
384 pwidg T Fin T 𝒫 T
385 3 384 syl φ T 𝒫 T
386 142 mptex n 0 c 0 n T | t T c t = n V
387 386 a1i φ n 0 c 0 n T | t T c t = n V
388 8 383 385 387 fvmptd3 φ D T = n 0 c 0 n T | t T c t = n
389 9 a1i φ C = n 0 c 0 n T | t T c t = n
390 388 389 eqtr4d φ D T = C
391 390 fveq1d φ D T N = C N
392 391 sumeq1d φ c D T N N ! t T c t ! t T S D n H t c t x = c C N N ! t T c t ! t T S D n H t c t x
393 392 mpteq2dv φ x X c D T N N ! t T c t ! t T S D n H t c t x = x X c C N N ! t T c t ! t T S D n H t c t x
394 375 393 eqtrd φ S D n F N = x X c C N N ! t T c t ! t T S D n H t c t x