Metamath Proof Explorer


Theorem dvmulbr

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Avoid ax-mulf and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses dvadd.f φ F : X
dvadd.x φ X S
dvadd.g φ G : Y
dvadd.y φ Y S
dvaddbr.s φ S
dvadd.bf φ C F S K
dvadd.bg φ C G S L
dvadd.j J = TopOpen fld
Assertion dvmulbr φ C F × f G S K G C + L F C

Proof

Step Hyp Ref Expression
1 dvadd.f φ F : X
2 dvadd.x φ X S
3 dvadd.g φ G : Y
4 dvadd.y φ Y S
5 dvaddbr.s φ S
6 dvadd.bf φ C F S K
7 dvadd.bg φ C G S L
8 dvadd.j J = TopOpen fld
9 eqid J 𝑡 S = J 𝑡 S
10 eqid z X C F z F C z C = z X C F z F C z C
11 9 8 10 5 1 2 eldv φ C F S K C int J 𝑡 S X K z X C F z F C z C lim C
12 6 11 mpbid φ C int J 𝑡 S X K z X C F z F C z C lim C
13 12 simpld φ C int J 𝑡 S X
14 eqid z Y C G z G C z C = z Y C G z G C z C
15 9 8 14 5 3 4 eldv φ C G S L C int J 𝑡 S Y L z Y C G z G C z C lim C
16 7 15 mpbid φ C int J 𝑡 S Y L z Y C G z G C z C lim C
17 16 simpld φ C int J 𝑡 S Y
18 13 17 elind φ C int J 𝑡 S X int J 𝑡 S Y
19 8 cnfldtopon J TopOn
20 resttopon J TopOn S J 𝑡 S TopOn S
21 19 5 20 sylancr φ J 𝑡 S TopOn S
22 topontop J 𝑡 S TopOn S J 𝑡 S Top
23 21 22 syl φ J 𝑡 S Top
24 toponuni J 𝑡 S TopOn S S = J 𝑡 S
25 21 24 syl φ S = J 𝑡 S
26 2 25 sseqtrd φ X J 𝑡 S
27 4 25 sseqtrd φ Y J 𝑡 S
28 eqid J 𝑡 S = J 𝑡 S
29 28 ntrin J 𝑡 S Top X J 𝑡 S Y J 𝑡 S int J 𝑡 S X Y = int J 𝑡 S X int J 𝑡 S Y
30 23 26 27 29 syl3anc φ int J 𝑡 S X Y = int J 𝑡 S X int J 𝑡 S Y
31 18 30 eleqtrrd φ C int J 𝑡 S X Y
32 1 adantr φ z X Y C F : X
33 inss1 X Y X
34 eldifi z X Y C z X Y
35 34 adantl φ z X Y C z X Y
36 33 35 sselid φ z X Y C z X
37 32 36 ffvelcdmd φ z X Y C F z
38 5 1 2 dvbss φ dom F S X
39 reldv Rel F S
40 releldm Rel F S C F S K C dom F S
41 39 6 40 sylancr φ C dom F S
42 38 41 sseldd φ C X
43 1 42 ffvelcdmd φ F C
44 43 adantr φ z X Y C F C
45 37 44 subcld φ z X Y C F z F C
46 2 5 sstrd φ X
47 46 adantr φ z X Y C X
48 47 36 sseldd φ z X Y C z
49 46 42 sseldd φ C
50 49 adantr φ z X Y C C
51 48 50 subcld φ z X Y C z C
52 eldifsni z X Y C z C
53 52 adantl φ z X Y C z C
54 48 50 53 subne0d φ z X Y C z C 0
55 45 51 54 divcld φ z X Y C F z F C z C
56 3 adantr φ z X Y C G : Y
57 inss2 X Y Y
58 57 35 sselid φ z X Y C z Y
59 56 58 ffvelcdmd φ z X Y C G z
60 55 59 mulcld φ z X Y C F z F C z C G z
61 ssdif X Y Y X Y C Y C
62 57 61 mp1i φ X Y C Y C
63 62 sselda φ z X Y C z Y C
64 4 5 sstrd φ Y
65 5 3 4 dvbss φ dom G S Y
66 reldv Rel G S
67 releldm Rel G S C G S L C dom G S
68 66 7 67 sylancr φ C dom G S
69 65 68 sseldd φ C Y
70 3 64 69 dvlem φ z Y C G z G C z C
71 63 70 syldan φ z X Y C G z G C z C
72 71 44 mulcld φ z X Y C G z G C z C F C
73 ssidd φ
74 txtopon J TopOn J TopOn J × t J TopOn ×
75 19 19 74 mp2an J × t J TopOn ×
76 75 toponrestid J × t J = J × t J 𝑡 ×
77 12 simprd φ K z X C F z F C z C lim C
78 1 46 42 dvlem φ z X C F z F C z C
79 78 fmpttd φ z X C F z F C z C : X C
80 ssdif X Y X X Y C X C
81 33 80 mp1i φ X Y C X C
82 46 ssdifssd φ X C
83 eqid J 𝑡 X C C = J 𝑡 X C C
84 33 2 sstrid φ X Y S
85 84 25 sseqtrd φ X Y J 𝑡 S
86 difssd φ J 𝑡 S X J 𝑡 S
87 85 86 unssd φ X Y J 𝑡 S X J 𝑡 S
88 ssun1 X Y X Y J 𝑡 S X
89 88 a1i φ X Y X Y J 𝑡 S X
90 28 ntrss J 𝑡 S Top X Y J 𝑡 S X J 𝑡 S X Y X Y J 𝑡 S X int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S X
91 23 87 89 90 syl3anc φ int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S X
92 eqid x X C F x F C x C = x X C F x F C x C
93 9 8 92 5 1 2 eldv φ C F S K C int J 𝑡 S X K x X C F x F C x C lim C
94 6 93 mpbid φ C int J 𝑡 S X K x X C F x F C x C lim C
95 94 simpld φ C int J 𝑡 S X
96 eqid x Y C G x G C x C = x Y C G x G C x C
97 9 8 96 5 3 4 eldv φ C G S L C int J 𝑡 S Y L x Y C G x G C x C lim C
98 7 97 mpbid φ C int J 𝑡 S Y L x Y C G x G C x C lim C
99 98 simpld φ C int J 𝑡 S Y
100 95 99 elind φ C int J 𝑡 S X int J 𝑡 S Y
101 100 30 eleqtrrd φ C int J 𝑡 S X Y
102 91 101 sseldd φ C int J 𝑡 S X Y J 𝑡 S X
103 102 42 elind φ C int J 𝑡 S X Y J 𝑡 S X X
104 33 a1i φ X Y X
105 eqid J 𝑡 S 𝑡 X = J 𝑡 S 𝑡 X
106 28 105 restntr J 𝑡 S Top X J 𝑡 S X Y X int J 𝑡 S 𝑡 X X Y = int J 𝑡 S X Y J 𝑡 S X X
107 23 26 104 106 syl3anc φ int J 𝑡 S 𝑡 X X Y = int J 𝑡 S X Y J 𝑡 S X X
108 8 cnfldtop J Top
109 108 a1i φ J Top
110 cnex V
111 ssexg S V S V
112 5 110 111 sylancl φ S V
113 restabs J Top X S S V J 𝑡 S 𝑡 X = J 𝑡 X
114 109 2 112 113 syl3anc φ J 𝑡 S 𝑡 X = J 𝑡 X
115 114 fveq2d φ int J 𝑡 S 𝑡 X = int J 𝑡 X
116 115 fveq1d φ int J 𝑡 S 𝑡 X X Y = int J 𝑡 X X Y
117 107 116 eqtr3d φ int J 𝑡 S X Y J 𝑡 S X X = int J 𝑡 X X Y
118 103 117 eleqtrd φ C int J 𝑡 X X Y
119 undif1 X C C = X C
120 42 snssd φ C X
121 ssequn2 C X X C = X
122 120 121 sylib φ X C = X
123 119 122 eqtrid φ X C C = X
124 123 oveq2d φ J 𝑡 X C C = J 𝑡 X
125 124 fveq2d φ int J 𝑡 X C C = int J 𝑡 X
126 undif1 X Y C C = X Y C
127 42 69 elind φ C X Y
128 127 snssd φ C X Y
129 ssequn2 C X Y X Y C = X Y
130 128 129 sylib φ X Y C = X Y
131 126 130 eqtrid φ X Y C C = X Y
132 125 131 fveq12d φ int J 𝑡 X C C X Y C C = int J 𝑡 X X Y
133 118 132 eleqtrrd φ C int J 𝑡 X C C X Y C C
134 79 81 82 8 83 133 limcres φ z X C F z F C z C X Y C lim C = z X C F z F C z C lim C
135 81 resmptd φ z X C F z F C z C X Y C = z X Y C F z F C z C
136 135 oveq1d φ z X C F z F C z C X Y C lim C = z X Y C F z F C z C lim C
137 134 136 eqtr3d φ z X C F z F C z C lim C = z X Y C F z F C z C lim C
138 77 137 eleqtrd φ K z X Y C F z F C z C lim C
139 eqid J 𝑡 Y = J 𝑡 Y
140 139 8 dvcnp2 S G : Y Y S C dom G S G J 𝑡 Y CnP J C
141 5 3 4 68 140 syl31anc φ G J 𝑡 Y CnP J C
142 8 139 cnplimc Y C Y G J 𝑡 Y CnP J C G : Y G C G lim C
143 64 69 142 syl2anc φ G J 𝑡 Y CnP J C G : Y G C G lim C
144 141 143 mpbid φ G : Y G C G lim C
145 144 simprd φ G C G lim C
146 difss X Y C X Y
147 146 57 sstri X Y C Y
148 147 a1i φ X Y C Y
149 eqid J 𝑡 Y C = J 𝑡 Y C
150 difssd φ J 𝑡 S Y J 𝑡 S
151 85 150 unssd φ X Y J 𝑡 S Y J 𝑡 S
152 ssun1 X Y X Y J 𝑡 S Y
153 152 a1i φ X Y X Y J 𝑡 S Y
154 28 ntrss J 𝑡 S Top X Y J 𝑡 S Y J 𝑡 S X Y X Y J 𝑡 S Y int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S Y
155 23 151 153 154 syl3anc φ int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S Y
156 155 101 sseldd φ C int J 𝑡 S X Y J 𝑡 S Y
157 156 69 elind φ C int J 𝑡 S X Y J 𝑡 S Y Y
158 57 a1i φ X Y Y
159 eqid J 𝑡 S 𝑡 Y = J 𝑡 S 𝑡 Y
160 28 159 restntr J 𝑡 S Top Y J 𝑡 S X Y Y int J 𝑡 S 𝑡 Y X Y = int J 𝑡 S X Y J 𝑡 S Y Y
161 23 27 158 160 syl3anc φ int J 𝑡 S 𝑡 Y X Y = int J 𝑡 S X Y J 𝑡 S Y Y
162 restabs J Top Y S S V J 𝑡 S 𝑡 Y = J 𝑡 Y
163 109 4 112 162 syl3anc φ J 𝑡 S 𝑡 Y = J 𝑡 Y
164 163 fveq2d φ int J 𝑡 S 𝑡 Y = int J 𝑡 Y
165 164 fveq1d φ int J 𝑡 S 𝑡 Y X Y = int J 𝑡 Y X Y
166 161 165 eqtr3d φ int J 𝑡 S X Y J 𝑡 S Y Y = int J 𝑡 Y X Y
167 157 166 eleqtrd φ C int J 𝑡 Y X Y
168 69 snssd φ C Y
169 ssequn2 C Y Y C = Y
170 168 169 sylib φ Y C = Y
171 170 oveq2d φ J 𝑡 Y C = J 𝑡 Y
172 171 fveq2d φ int J 𝑡 Y C = int J 𝑡 Y
173 172 131 fveq12d φ int J 𝑡 Y C X Y C C = int J 𝑡 Y X Y
174 167 173 eleqtrrd φ C int J 𝑡 Y C X Y C C
175 3 148 64 8 149 174 limcres φ G X Y C lim C = G lim C
176 3 148 feqresmpt φ G X Y C = z X Y C G z
177 176 oveq1d φ G X Y C lim C = z X Y C G z lim C
178 175 177 eqtr3d φ G lim C = z X Y C G z lim C
179 145 178 eleqtrd φ G C z X Y C G z lim C
180 8 mpomulcn u , v u v J × t J Cn J
181 5 1 2 dvcl φ C F S K K
182 6 181 mpdan φ K
183 3 69 ffvelcdmd φ G C
184 182 183 opelxpd φ K G C ×
185 75 toponunii × = J × t J
186 185 cncnpi u , v u v J × t J Cn J K G C × u , v u v J × t J CnP J K G C
187 180 184 186 sylancr φ u , v u v J × t J CnP J K G C
188 55 59 73 73 8 76 138 179 187 limccnp2 φ K u , v u v G C z X Y C F z F C z C u , v u v G z lim C
189 df-mpt z X Y C F z F C z C u , v u v G z = z w | z X Y C w = F z F C z C u , v u v G z
190 189 oveq1i z X Y C F z F C z C u , v u v G z lim C = z w | z X Y C w = F z F C z C u , v u v G z lim C
191 188 190 eleqtrdi φ K u , v u v G C z w | z X Y C w = F z F C z C u , v u v G z lim C
192 ovmpot K G C K u , v u v G C = K G C
193 182 183 192 syl2anc φ K u , v u v G C = K G C
194 ovmpot F z F C z C G z F z F C z C u , v u v G z = F z F C z C G z
195 55 59 194 syl2anc φ z X Y C F z F C z C u , v u v G z = F z F C z C G z
196 195 eqeq2d φ z X Y C w = F z F C z C u , v u v G z w = F z F C z C G z
197 196 pm5.32da φ z X Y C w = F z F C z C u , v u v G z z X Y C w = F z F C z C G z
198 197 opabbidv φ z w | z X Y C w = F z F C z C u , v u v G z = z w | z X Y C w = F z F C z C G z
199 df-mpt z X Y C F z F C z C G z = z w | z X Y C w = F z F C z C G z
200 198 199 eqtr4di φ z w | z X Y C w = F z F C z C u , v u v G z = z X Y C F z F C z C G z
201 200 oveq1d φ z w | z X Y C w = F z F C z C u , v u v G z lim C = z X Y C F z F C z C G z lim C
202 191 193 201 3eltr3d φ K G C z X Y C F z F C z C G z lim C
203 16 simprd φ L z Y C G z G C z C lim C
204 70 fmpttd φ z Y C G z G C z C : Y C
205 64 ssdifssd φ Y C
206 eqid J 𝑡 Y C C = J 𝑡 Y C C
207 undif1 Y C C = Y C
208 207 170 eqtrid φ Y C C = Y
209 208 oveq2d φ J 𝑡 Y C C = J 𝑡 Y
210 209 fveq2d φ int J 𝑡 Y C C = int J 𝑡 Y
211 210 131 fveq12d φ int J 𝑡 Y C C X Y C C = int J 𝑡 Y X Y
212 167 211 eleqtrrd φ C int J 𝑡 Y C C X Y C C
213 204 62 205 8 206 212 limcres φ z Y C G z G C z C X Y C lim C = z Y C G z G C z C lim C
214 62 resmptd φ z Y C G z G C z C X Y C = z X Y C G z G C z C
215 214 oveq1d φ z Y C G z G C z C X Y C lim C = z X Y C G z G C z C lim C
216 213 215 eqtr3d φ z Y C G z G C z C lim C = z X Y C G z G C z C lim C
217 203 216 eleqtrd φ L z X Y C G z G C z C lim C
218 84 5 sstrd φ X Y
219 cncfmptc F C X Y z X Y F C : X Y cn
220 43 218 73 219 syl3anc φ z X Y F C : X Y cn
221 eqidd z = C F C = F C
222 220 127 221 cnmptlimc φ F C z X Y F C lim C
223 43 adantr φ z X Y F C
224 223 fmpttd φ z X Y F C : X Y
225 224 limcdif φ z X Y F C lim C = z X Y F C X Y C lim C
226 resmpt X Y C X Y z X Y F C X Y C = z X Y C F C
227 146 226 mp1i φ z X Y F C X Y C = z X Y C F C
228 227 oveq1d φ z X Y F C X Y C lim C = z X Y C F C lim C
229 225 228 eqtrd φ z X Y F C lim C = z X Y C F C lim C
230 222 229 eleqtrd φ F C z X Y C F C lim C
231 5 3 4 dvcl φ C G S L L
232 7 231 mpdan φ L
233 232 43 opelxpd φ L F C ×
234 185 cncnpi u , v u v J × t J Cn J L F C × u , v u v J × t J CnP J L F C
235 180 233 234 sylancr φ u , v u v J × t J CnP J L F C
236 71 44 73 73 8 76 217 230 235 limccnp2 φ L u , v u v F C z X Y C G z G C z C u , v u v F C lim C
237 df-mpt z X Y C G z G C z C u , v u v F C = z w | z X Y C w = G z G C z C u , v u v F C
238 237 oveq1i z X Y C G z G C z C u , v u v F C lim C = z w | z X Y C w = G z G C z C u , v u v F C lim C
239 236 238 eleqtrdi φ L u , v u v F C z w | z X Y C w = G z G C z C u , v u v F C lim C
240 ovmpot L F C L u , v u v F C = L F C
241 232 43 240 syl2anc φ L u , v u v F C = L F C
242 42 adantr φ z X Y C C X
243 32 242 ffvelcdmd φ z X Y C F C
244 ovmpot G z G C z C F C G z G C z C u , v u v F C = G z G C z C F C
245 71 243 244 syl2anc φ z X Y C G z G C z C u , v u v F C = G z G C z C F C
246 245 eqeq2d φ z X Y C w = G z G C z C u , v u v F C w = G z G C z C F C
247 246 pm5.32da φ z X Y C w = G z G C z C u , v u v F C z X Y C w = G z G C z C F C
248 247 opabbidv φ z w | z X Y C w = G z G C z C u , v u v F C = z w | z X Y C w = G z G C z C F C
249 df-mpt z X Y C G z G C z C F C = z w | z X Y C w = G z G C z C F C
250 248 249 eqtr4di φ z w | z X Y C w = G z G C z C u , v u v F C = z X Y C G z G C z C F C
251 250 oveq1d φ z w | z X Y C w = G z G C z C u , v u v F C lim C = z X Y C G z G C z C F C lim C
252 239 241 251 3eltr3d φ L F C z X Y C G z G C z C F C lim C
253 8 addcn + J × t J Cn J
254 182 183 mulcld φ K G C
255 232 43 mulcld φ L F C
256 254 255 opelxpd φ K G C L F C ×
257 185 cncnpi + J × t J Cn J K G C L F C × + J × t J CnP J K G C L F C
258 253 256 257 sylancr φ + J × t J CnP J K G C L F C
259 60 72 73 73 8 76 202 252 258 limccnp2 φ K G C + L F C z X Y C F z F C z C G z + G z G C z C F C lim C
260 37 243 subcld φ z X Y C F z F C
261 260 59 mulcld φ z X Y C F z F C G z
262 69 adantr φ z X Y C C Y
263 56 262 ffvelcdmd φ z X Y C G C
264 59 263 subcld φ z X Y C G z G C
265 264 243 mulcld φ z X Y C G z G C F C
266 47 242 sseldd φ z X Y C C
267 48 266 subcld φ z X Y C z C
268 261 265 267 54 divdird φ z X Y C F z F C G z + G z G C F C z C = F z F C G z z C + G z G C F C z C
269 37 59 mulcld φ z X Y C F z G z
270 243 59 mulcld φ z X Y C F C G z
271 243 263 mulcld φ z X Y C F C G C
272 269 270 271 npncand φ z X Y C F z G z F C G z + F C G z - F C G C = F z G z F C G C
273 37 243 59 subdird φ z X Y C F z F C G z = F z G z F C G z
274 264 243 mulcomd φ z X Y C G z G C F C = F C G z G C
275 243 59 263 subdid φ z X Y C F C G z G C = F C G z F C G C
276 274 275 eqtrd φ z X Y C G z G C F C = F C G z F C G C
277 273 276 oveq12d φ z X Y C F z F C G z + G z G C F C = F z G z F C G z + F C G z - F C G C
278 1 ffnd φ F Fn X
279 278 adantr φ z X Y C F Fn X
280 3 ffnd φ G Fn Y
281 280 adantr φ z X Y C G Fn Y
282 ssexg X V X V
283 46 110 282 sylancl φ X V
284 283 adantr φ z X Y C X V
285 ssexg Y V Y V
286 64 110 285 sylancl φ Y V
287 286 adantr φ z X Y C Y V
288 eqid X Y = X Y
289 eqidd φ z X Y C z X F z = F z
290 eqidd φ z X Y C z Y G z = G z
291 279 281 284 287 288 289 290 ofval φ z X Y C z X Y F × f G z = F z G z
292 35 291 mpdan φ z X Y C F × f G z = F z G z
293 eqidd φ z X Y C C X F C = F C
294 eqidd φ z X Y C C Y G C = G C
295 279 281 284 287 288 293 294 ofval φ z X Y C C X Y F × f G C = F C G C
296 127 295 mpidan φ z X Y C F × f G C = F C G C
297 292 296 oveq12d φ z X Y C F × f G z F × f G C = F z G z F C G C
298 272 277 297 3eqtr4d φ z X Y C F z F C G z + G z G C F C = F × f G z F × f G C
299 298 oveq1d φ z X Y C F z F C G z + G z G C F C z C = F × f G z F × f G C z C
300 260 59 267 54 div23d φ z X Y C F z F C G z z C = F z F C z C G z
301 264 243 267 54 div23d φ z X Y C G z G C F C z C = G z G C z C F C
302 300 301 oveq12d φ z X Y C F z F C G z z C + G z G C F C z C = F z F C z C G z + G z G C z C F C
303 268 299 302 3eqtr3d φ z X Y C F × f G z F × f G C z C = F z F C z C G z + G z G C z C F C
304 303 mpteq2dva φ z X Y C F × f G z F × f G C z C = z X Y C F z F C z C G z + G z G C z C F C
305 304 oveq1d φ z X Y C F × f G z F × f G C z C lim C = z X Y C F z F C z C G z + G z G C z C F C lim C
306 259 305 eleqtrrd φ K G C + L F C z X Y C F × f G z F × f G C z C lim C
307 eqid z X Y C F × f G z F × f G C z C = z X Y C F × f G z F × f G C z C
308 mulcl x y x y
309 308 adantl φ x y x y
310 309 1 3 283 286 288 off φ F × f G : X Y
311 9 8 307 5 310 84 eldv φ C F × f G S K G C + L F C C int J 𝑡 S X Y K G C + L F C z X Y C F × f G z F × f G C z C lim C
312 31 306 311 mpbir2and φ C F × f G S K G C + L F C