Metamath Proof Explorer


Theorem dvmptfprod

Description: Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptfprod.iph i φ
dvmptfprod.jph j φ
dvmptfprod.j J = K 𝑡 S
dvmptfprod.k K = TopOpen fld
dvmptfprod.s φ S
dvmptfprod.x φ X J
dvmptfprod.i φ I Fin
dvmptfprod.a φ i I x X A
dvmptfprod.b φ i I x X B
dvmptfprod.d φ i I dx X A dS x = x X B
dvmptfprod.bc i = j B = C
Assertion dvmptfprod φ dx X i I A dS x = x X j I C i I j A

Proof

Step Hyp Ref Expression
1 dvmptfprod.iph i φ
2 dvmptfprod.jph j φ
3 dvmptfprod.j J = K 𝑡 S
4 dvmptfprod.k K = TopOpen fld
5 dvmptfprod.s φ S
6 dvmptfprod.x φ X J
7 dvmptfprod.i φ I Fin
8 dvmptfprod.a φ i I x X A
9 dvmptfprod.b φ i I x X B
10 dvmptfprod.d φ i I dx X A dS x = x X B
11 dvmptfprod.bc i = j B = C
12 ssid I I
13 12 jctr φ φ I I
14 sseq1 a = a I I
15 14 anbi2d a = φ a I φ I
16 prodeq1 a = i a A = i A
17 16 mpteq2dv a = x X i a A = x X i A
18 17 oveq2d a = dx X i a A dS x = dx X i A dS x
19 sumeq1 a = j a C i a j A = j C i a j A
20 difeq1 a = a j = j
21 20 prodeq1d a = i a j A = i j A
22 21 oveq2d a = C i a j A = C i j A
23 22 sumeq2sdv a = j C i a j A = j C i j A
24 19 23 eqtrd a = j a C i a j A = j C i j A
25 24 mpteq2dv a = x X j a C i a j A = x X j C i j A
26 18 25 eqeq12d a = dx X i a A dS x = x X j a C i a j A dx X i A dS x = x X j C i j A
27 15 26 imbi12d a = φ a I dx X i a A dS x = x X j a C i a j A φ I dx X i A dS x = x X j C i j A
28 sseq1 a = b a I b I
29 28 anbi2d a = b φ a I φ b I
30 prodeq1 a = b i a A = i b A
31 30 mpteq2dv a = b x X i a A = x X i b A
32 31 oveq2d a = b dx X i a A dS x = dx X i b A dS x
33 sumeq1 a = b j a C i a j A = j b C i a j A
34 difeq1 a = b a j = b j
35 34 prodeq1d a = b i a j A = i b j A
36 35 oveq2d a = b C i a j A = C i b j A
37 36 sumeq2sdv a = b j b C i a j A = j b C i b j A
38 33 37 eqtrd a = b j a C i a j A = j b C i b j A
39 38 mpteq2dv a = b x X j a C i a j A = x X j b C i b j A
40 32 39 eqeq12d a = b dx X i a A dS x = x X j a C i a j A dx X i b A dS x = x X j b C i b j A
41 29 40 imbi12d a = b φ a I dx X i a A dS x = x X j a C i a j A φ b I dx X i b A dS x = x X j b C i b j A
42 sseq1 a = b c a I b c I
43 42 anbi2d a = b c φ a I φ b c I
44 prodeq1 a = b c i a A = i b c A
45 44 mpteq2dv a = b c x X i a A = x X i b c A
46 45 oveq2d a = b c dx X i a A dS x = dx X i b c A dS x
47 sumeq1 a = b c j a C i a j A = j b c C i a j A
48 difeq1 a = b c a j = b c j
49 48 prodeq1d a = b c i a j A = i b c j A
50 49 oveq2d a = b c C i a j A = C i b c j A
51 50 sumeq2sdv a = b c j b c C i a j A = j b c C i b c j A
52 47 51 eqtrd a = b c j a C i a j A = j b c C i b c j A
53 52 mpteq2dv a = b c x X j a C i a j A = x X j b c C i b c j A
54 46 53 eqeq12d a = b c dx X i a A dS x = x X j a C i a j A dx X i b c A dS x = x X j b c C i b c j A
55 43 54 imbi12d a = b c φ a I dx X i a A dS x = x X j a C i a j A φ b c I dx X i b c A dS x = x X j b c C i b c j A
56 sseq1 a = I a I I I
57 56 anbi2d a = I φ a I φ I I
58 prodeq1 a = I i a A = i I A
59 58 mpteq2dv a = I x X i a A = x X i I A
60 59 oveq2d a = I dx X i a A dS x = dx X i I A dS x
61 sumeq1 a = I j a C i a j A = j I C i a j A
62 difeq1 a = I a j = I j
63 62 prodeq1d a = I i a j A = i I j A
64 63 oveq2d a = I C i a j A = C i I j A
65 64 a1d a = I j I C i a j A = C i I j A
66 65 ralrimiv a = I j I C i a j A = C i I j A
67 66 sumeq2d a = I j I C i a j A = j I C i I j A
68 61 67 eqtrd a = I j a C i a j A = j I C i I j A
69 68 mpteq2dv a = I x X j a C i a j A = x X j I C i I j A
70 60 69 eqeq12d a = I dx X i a A dS x = x X j a C i a j A dx X i I A dS x = x X j I C i I j A
71 57 70 imbi12d a = I φ a I dx X i a A dS x = x X j a C i a j A φ I I dx X i I A dS x = x X j I C i I j A
72 prod0 i A = 1
73 72 mpteq2i x X i A = x X 1
74 73 oveq2i dx X i A dS x = dx X 1 dS x
75 74 a1i φ dx X i A dS x = dx X 1 dS x
76 4 oveq1i K 𝑡 S = TopOpen fld 𝑡 S
77 3 76 eqtri J = TopOpen fld 𝑡 S
78 6 77 eleqtrdi φ X TopOpen fld 𝑡 S
79 1cnd φ 1
80 5 78 79 dvmptconst φ dx X 1 dS x = x X 0
81 sum0 j C i j A = 0
82 81 eqcomi 0 = j C i j A
83 82 mpteq2i x X 0 = x X j C i j A
84 83 a1i φ x X 0 = x X j C i j A
85 75 80 84 3eqtrd φ dx X i A dS x = x X j C i j A
86 85 adantr φ I dx X i A dS x = x X j C i j A
87 simp3 b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I φ b c I
88 simp1r b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I ¬ c b
89 simpl φ b c I φ
90 ssun1 b b c
91 sstr2 b b c b c I b I
92 90 91 ax-mp b c I b I
93 92 adantl φ b c I b I
94 89 93 jca φ b c I φ b I
95 94 adantl φ b I dx X i b A dS x = x X j b C i b j A φ b c I φ b I
96 simpl φ b I dx X i b A dS x = x X j b C i b j A φ b c I φ b I dx X i b A dS x = x X j b C i b j A
97 95 96 mpd φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b A dS x = x X j b C i b j A
98 97 3adant1 b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b A dS x = x X j b C i b j A
99 nfv x φ b c I ¬ c b
100 nfcv _ x S
101 nfcv _ x D
102 nfmpt1 _ x x X i b A
103 100 101 102 nfov _ x dx X i b A dS x
104 nfmpt1 _ x x X j b C i b j A
105 103 104 nfeq x dx X i b A dS x = x X j b C i b j A
106 99 105 nfan x φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A
107 nfv i b c I
108 1 107 nfan i φ b c I
109 nfv i ¬ c b
110 108 109 nfan i φ b c I ¬ c b
111 nfcv _ i S
112 nfcv _ i D
113 nfcv _ i X
114 nfcv _ i b
115 114 nfcprod1 _ i i b A
116 113 115 nfmpt _ i x X i b A
117 111 112 116 nfov _ i dx X i b A dS x
118 nfcv _ i C
119 nfcv _ i ×
120 nfcv _ i b j
121 120 nfcprod1 _ i i b j A
122 118 119 121 nfov _ i C i b j A
123 114 122 nfsum _ i j b C i b j A
124 113 123 nfmpt _ i x X j b C i b j A
125 117 124 nfeq i dx X i b A dS x = x X j b C i b j A
126 110 125 nfan i φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A
127 nfv j b c I
128 2 127 nfan j φ b c I
129 nfv j ¬ c b
130 128 129 nfan j φ b c I ¬ c b
131 nfcv _ j dx X i b A dS x
132 nfcv _ j X
133 nfcv _ j b
134 133 nfsum1 _ j j b C i b j A
135 132 134 nfmpt _ j x X j b C i b j A
136 131 135 nfeq j dx X i b A dS x = x X j b C i b j A
137 130 136 nfan j φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A
138 nfcsb1v _ i c / i A
139 nfcsb1v _ j c / j C
140 89 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A φ
141 140 3ad2ant1 φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A i I x X φ
142 simp2 φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A i I x X i I
143 simp3 φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A i I x X x X
144 141 142 143 8 syl3anc φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A i I x X A
145 140 7 syl φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A I Fin
146 93 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A b I
147 ssfi I Fin b I b Fin
148 145 146 147 syl2anc φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A b Fin
149 vex c V
150 149 a1i φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A c V
151 simplr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A ¬ c b
152 simpllr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A b c I
153 5 ad3antrrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A S
154 140 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b φ
155 146 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b b I
156 simpr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b j b
157 155 156 sseldd φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b j I
158 simplr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b x X
159 nfv i j I
160 nfv i x X
161 1 159 160 nf3an i φ j I x X
162 nfv i C
163 161 162 nfim i φ j I x X C
164 eleq1w i = j i I j I
165 164 3anbi2d i = j φ i I x X φ j I x X
166 11 eleq1d i = j B C
167 165 166 imbi12d i = j φ i I x X B φ j I x X C
168 163 167 9 chvarfv φ j I x X C
169 154 157 158 168 syl3anc φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b C
170 simpr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A dx X i b A dS x = x X j b C i b j A
171 89 adantr φ b c I x X φ
172 id b c I b c I
173 149 snid c c
174 elun2 c c c b c
175 173 174 ax-mp c b c
176 175 a1i b c I c b c
177 172 176 sseldd b c I c I
178 177 ad2antlr φ b c I x X c I
179 simpr φ b c I x X x X
180 nfv j c I
181 nfv j x X
182 2 180 181 nf3an j φ c I x X
183 nfcv _ j
184 139 183 nfel j c / j C
185 182 184 nfim j φ c I x X c / j C
186 eleq1w j = c j I c I
187 186 3anbi2d j = c φ j I x X φ c I x X
188 csbeq1a j = c C = c / j C
189 188 eleq1d j = c C c / j C
190 187 189 imbi12d j = c φ j I x X C φ c I x X c / j C
191 185 190 168 chvarfv φ c I x X c / j C
192 171 178 179 191 syl3anc φ b c I x X c / j C
193 192 adantlr φ b c I ¬ c b x X c / j C
194 193 adantlr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X c / j C
195 2 180 nfan j φ c I
196 nfcv _ j dx X c / i A dS x
197 132 139 nfmpt _ j x X c / j C
198 196 197 nfeq j dx X c / i A dS x = x X c / j C
199 195 198 nfim j φ c I dx X c / i A dS x = x X c / j C
200 186 anbi2d j = c φ j I φ c I
201 csbeq1a j = c j / i A = c / j j / i A
202 csbcow c / j j / i A = c / i A
203 202 a1i j = c c / j j / i A = c / i A
204 201 203 eqtrd j = c j / i A = c / i A
205 204 mpteq2dv j = c x X j / i A = x X c / i A
206 205 oveq2d j = c dx X j / i A dS x = dx X c / i A dS x
207 188 mpteq2dv j = c x X C = x X c / j C
208 206 207 eqeq12d j = c dx X j / i A dS x = x X C dx X c / i A dS x = x X c / j C
209 200 208 imbi12d j = c φ j I dx X j / i A dS x = x X C φ c I dx X c / i A dS x = x X c / j C
210 1 159 nfan i φ j I
211 nfcsb1v _ i j / i A
212 113 211 nfmpt _ i x X j / i A
213 111 112 212 nfov _ i dx X j / i A dS x
214 nfcv _ i x X C
215 213 214 nfeq i dx X j / i A dS x = x X C
216 210 215 nfim i φ j I dx X j / i A dS x = x X C
217 164 anbi2d i = j φ i I φ j I
218 csbeq1a i = j A = j / i A
219 218 mpteq2dv i = j x X A = x X j / i A
220 219 oveq2d i = j dx X A dS x = dx X j / i A dS x
221 11 idi i = j B = C
222 221 mpteq2dv i = j x X B = x X C
223 220 222 eqeq12d i = j dx X A dS x = x X B dx X j / i A dS x = x X C
224 217 223 imbi12d i = j φ i I dx X A dS x = x X B φ j I dx X j / i A dS x = x X C
225 216 224 10 chvarfv φ j I dx X j / i A dS x = x X C
226 199 209 225 chvarfv φ c I dx X c / i A dS x = x X c / j C
227 177 226 sylan2 φ b c I dx X c / i A dS x = x X c / j C
228 227 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A dx X c / i A dS x = x X c / j C
229 csbeq1a i = c A = c / i A
230 106 126 137 138 139 144 148 150 151 152 153 169 170 194 228 229 188 dvmptfprodlem φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A dx X i b c A dS x = x X j b c C i b c j A
231 87 88 98 230 syl21anc b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b c A dS x = x X j b c C i b c j A
232 231 3exp b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b c A dS x = x X j b c C i b c j A
233 27 41 55 71 86 232 findcard2s I Fin φ I I dx X i I A dS x = x X j I C i I j A
234 7 13 233 sylc φ dx X i I A dS x = x X j I C i I j A