Metamath Proof Explorer


Theorem dvcobr

Description: The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco . (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 dvco.f φ F : X
dvco.x φ X S
dvco.g φ G : Y X
dvco.y φ Y T
dvcobr.s φ S
dvcobr.t φ T
dvco.bf φ G C F S K
dvco.bg φ C G T L
dvco.j J = TopOpen fld
Assertion dvcobr φ C F G T K L

Proof

Step Hyp Ref Expression
1 dvco.f φ F : X
2 dvco.x φ X S
3 dvco.g φ G : Y X
4 dvco.y φ Y T
5 dvcobr.s φ S
6 dvcobr.t φ T
7 dvco.bf φ G C F S K
8 dvco.bg φ C G T L
9 dvco.j J = TopOpen fld
10 eqid J 𝑡 T = J 𝑡 T
11 eqid z Y C G z G C z C = z Y C G z G C z C
12 2 5 sstrd φ X
13 3 12 fssd φ G : Y
14 10 9 11 6 13 4 eldv φ C G T L C int J 𝑡 T Y L z Y C G z G C z C lim C
15 8 14 mpbid φ C int J 𝑡 T Y L z Y C G z G C z C lim C
16 15 simpld φ C int J 𝑡 T Y
17 5 1 2 dvcl φ G C F S K K
18 7 17 mpdan φ K
19 18 ad2antrr φ z Y C G z = G C K
20 1 adantr φ z Y C F : X
21 eldifi z Y C z Y
22 ffvelcdm G : Y X z Y G z X
23 3 21 22 syl2an φ z Y C G z X
24 20 23 ffvelcdmd φ z Y C F G z
25 24 adantr φ z Y C ¬ G z = G C F G z
26 3 adantr φ z Y C G : Y X
27 6 13 4 dvbss φ dom G T Y
28 reldv Rel G T
29 releldm Rel G T C G T L C dom G T
30 28 8 29 sylancr φ C dom G T
31 27 30 sseldd φ C Y
32 31 adantr φ z Y C C Y
33 26 32 ffvelcdmd φ z Y C G C X
34 20 33 ffvelcdmd φ z Y C F G C
35 34 adantr φ z Y C ¬ G z = G C F G C
36 25 35 subcld φ z Y C ¬ G z = G C F G z F G C
37 13 ad2antrr φ z Y C ¬ G z = G C G : Y
38 21 ad2antlr φ z Y C ¬ G z = G C z Y
39 37 38 ffvelcdmd φ z Y C ¬ G z = G C G z
40 31 ad2antrr φ z Y C ¬ G z = G C C Y
41 37 40 ffvelcdmd φ z Y C ¬ G z = G C G C
42 39 41 subcld φ z Y C ¬ G z = G C G z G C
43 simpr φ z Y C ¬ G z = G C ¬ G z = G C
44 39 41 subeq0ad φ z Y C ¬ G z = G C G z G C = 0 G z = G C
45 44 necon3abid φ z Y C ¬ G z = G C G z G C 0 ¬ G z = G C
46 43 45 mpbird φ z Y C ¬ G z = G C G z G C 0
47 36 42 46 divcld φ z Y C ¬ G z = G C F G z F G C G z G C
48 19 47 ifclda φ z Y C if G z = G C K F G z F G C G z G C
49 4 6 sstrd φ Y
50 13 49 31 dvlem φ z Y C G z G C z C
51 ssidd φ
52 9 cnfldtopon J TopOn
53 txtopon J TopOn J TopOn J × t J TopOn ×
54 52 52 53 mp2an J × t J TopOn ×
55 54 toponrestid J × t J = J × t J 𝑡 ×
56 23 anim1i φ z Y C G z G C G z X G z G C
57 eldifsn G z X G C G z X G z G C
58 56 57 sylibr φ z Y C G z G C G z X G C
59 58 anasss φ z Y C G z G C G z X G C
60 eldifsni y X G C y G C
61 ifnefalse y G C if y = G C K F y F G C y G C = F y F G C y G C
62 60 61 syl y X G C if y = G C K F y F G C y G C = F y F G C y G C
63 62 adantl φ y X G C if y = G C K F y F G C y G C = F y F G C y G C
64 3 31 ffvelcdmd φ G C X
65 1 12 64 dvlem φ y X G C F y F G C y G C
66 63 65 eqeltrd φ y X G C if y = G C K F y F G C y G C
67 limcresi G lim C G Y C lim C
68 3 feqmptd φ G = z Y G z
69 68 reseq1d φ G Y C = z Y G z Y C
70 difss Y C Y
71 resmpt Y C Y z Y G z Y C = z Y C G z
72 70 71 ax-mp z Y G z Y C = z Y C G z
73 69 72 eqtrdi φ G Y C = z Y C G z
74 73 oveq1d φ G Y C lim C = z Y C G z lim C
75 67 74 sseqtrid φ G lim C z Y C G z lim C
76 eqid J 𝑡 Y = J 𝑡 Y
77 76 9 dvcnp2 T G : Y Y T C dom G T G J 𝑡 Y CnP J C
78 6 13 4 30 77 syl31anc φ G J 𝑡 Y CnP J C
79 9 76 cnplimc Y C Y G J 𝑡 Y CnP J C G : Y G C G lim C
80 49 31 79 syl2anc φ G J 𝑡 Y CnP J C G : Y G C G lim C
81 78 80 mpbid φ G : Y G C G lim C
82 81 simprd φ G C G lim C
83 75 82 sseldd φ G C z Y C G z lim C
84 eqid J 𝑡 S = J 𝑡 S
85 eqid y X G C F y F G C y G C = y X G C F y F G C y G C
86 84 9 85 5 1 2 eldv φ G C F S K G C int J 𝑡 S X K y X G C F y F G C y G C lim G C
87 7 86 mpbid φ G C int J 𝑡 S X K y X G C F y F G C y G C lim G C
88 87 simprd φ K y X G C F y F G C y G C lim G C
89 62 mpteq2ia y X G C if y = G C K F y F G C y G C = y X G C F y F G C y G C
90 89 oveq1i y X G C if y = G C K F y F G C y G C lim G C = y X G C F y F G C y G C lim G C
91 88 90 eleqtrrdi φ K y X G C if y = G C K F y F G C y G C lim G C
92 eqeq1 y = G z y = G C G z = G C
93 fveq2 y = G z F y = F G z
94 93 oveq1d y = G z F y F G C = F G z F G C
95 oveq1 y = G z y G C = G z G C
96 94 95 oveq12d y = G z F y F G C y G C = F G z F G C G z G C
97 92 96 ifbieq2d y = G z if y = G C K F y F G C y G C = if G z = G C K F G z F G C G z G C
98 iftrue G z = G C if G z = G C K F G z F G C G z G C = K
99 98 ad2antll φ z Y C G z = G C if G z = G C K F G z F G C G z G C = K
100 59 66 83 91 97 99 limcco φ K z Y C if G z = G C K F G z F G C G z G C lim C
101 15 simprd φ L z Y C G z G C z C lim C
102 9 mpomulcn u , v u v J × t J Cn J
103 6 13 4 dvcl φ C G T L L
104 8 103 mpdan φ L
105 18 104 opelxpd φ K L ×
106 54 toponunii × = J × t J
107 106 cncnpi u , v u v J × t J Cn J K L × u , v u v J × t J CnP J K L
108 102 105 107 sylancr φ u , v u v J × t J CnP J K L
109 48 50 51 51 9 55 100 101 108 limccnp2 φ K u , v u v L z Y C if G z = G C K F G z F G C G z G C u , v u v G z G C z C lim C
110 df-mpt z Y C if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C
111 110 oveq1i z Y C if G z = G C K F G z F G C G z G C u , v u v G z G C z C lim C = z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C lim C
112 109 111 eleqtrdi φ K u , v u v L z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C lim C
113 ovmpot K L K u , v u v L = K L
114 18 104 113 syl2anc φ K u , v u v L = K L
115 ovmpot if G z = G C K F G z F G C G z G C G z G C z C if G z = G C K F G z F G C G z G C u , v u v G z G C z C = if G z = G C K F G z F G C G z G C G z G C z C
116 48 50 115 syl2anc φ z Y C if G z = G C K F G z F G C G z G C u , v u v G z G C z C = if G z = G C K F G z F G C G z G C G z G C z C
117 116 eqeq2d φ z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C w = if G z = G C K F G z F G C G z G C G z G C z C
118 117 pm5.32da φ z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C z Y C w = if G z = G C K F G z F G C G z G C G z G C z C
119 118 opabbidv φ z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z w | z Y C w = if G z = G C K F G z F G C G z G C G z G C z C
120 df-mpt z Y C if G z = G C K F G z F G C G z G C G z G C z C = z w | z Y C w = if G z = G C K F G z F G C G z G C G z G C z C
121 120 eqcomi z w | z Y C w = if G z = G C K F G z F G C G z G C G z G C z C = z Y C if G z = G C K F G z F G C G z G C G z G C z C
122 121 eqeq2i z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z w | z Y C w = if G z = G C K F G z F G C G z G C G z G C z C z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z Y C if G z = G C K F G z F G C G z G C G z G C z C
123 122 biimpi z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z w | z Y C w = if G z = G C K F G z F G C G z G C G z G C z C z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z Y C if G z = G C K F G z F G C G z G C G z G C z C
124 123 oveq1d z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C = z w | z Y C w = if G z = G C K F G z F G C G z G C G z G C z C z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C lim C = z Y C if G z = G C K F G z F G C G z G C G z G C z C lim C
125 119 124 syl φ z w | z Y C w = if G z = G C K F G z F G C G z G C u , v u v G z G C z C lim C = z Y C if G z = G C K F G z F G C G z G C G z G C z C lim C
126 112 114 125 3eltr3d φ K L z Y C if G z = G C K F G z F G C G z G C G z G C z C lim C
127 oveq1 K = if G z = G C K F G z F G C G z G C K G z G C z C = if G z = G C K F G z F G C G z G C G z G C z C
128 127 eqeq1d K = if G z = G C K F G z F G C G z G C K G z G C z C = F G z F G C z C if G z = G C K F G z F G C G z G C G z G C z C = F G z F G C z C
129 oveq1 F G z F G C G z G C = if G z = G C K F G z F G C G z G C F G z F G C G z G C G z G C z C = if G z = G C K F G z F G C G z G C G z G C z C
130 129 eqeq1d F G z F G C G z G C = if G z = G C K F G z F G C G z G C F G z F G C G z G C G z G C z C = F G z F G C z C if G z = G C K F G z F G C G z G C G z G C z C = F G z F G C z C
131 19 mul01d φ z Y C G z = G C K 0 = 0
132 12 adantr φ z Y C X
133 132 23 sseldd φ z Y C G z
134 132 33 sseldd φ z Y C G C
135 133 134 subeq0ad φ z Y C G z G C = 0 G z = G C
136 135 biimpar φ z Y C G z = G C G z G C = 0
137 136 oveq1d φ z Y C G z = G C G z G C z C = 0 z C
138 49 adantr φ z Y C Y
139 21 adantl φ z Y C z Y
140 138 139 sseldd φ z Y C z
141 138 32 sseldd φ z Y C C
142 140 141 subcld φ z Y C z C
143 eldifsni z Y C z C
144 143 adantl φ z Y C z C
145 140 141 144 subne0d φ z Y C z C 0
146 142 145 div0d φ z Y C 0 z C = 0
147 146 adantr φ z Y C G z = G C 0 z C = 0
148 137 147 eqtrd φ z Y C G z = G C G z G C z C = 0
149 148 oveq2d φ z Y C G z = G C K G z G C z C = K 0
150 fveq2 G z = G C F G z = F G C
151 24 34 subeq0ad φ z Y C F G z F G C = 0 F G z = F G C
152 150 151 imbitrrid φ z Y C G z = G C F G z F G C = 0
153 152 imp φ z Y C G z = G C F G z F G C = 0
154 153 oveq1d φ z Y C G z = G C F G z F G C z C = 0 z C
155 154 147 eqtrd φ z Y C G z = G C F G z F G C z C = 0
156 131 149 155 3eqtr4d φ z Y C G z = G C K G z G C z C = F G z F G C z C
157 142 adantr φ z Y C ¬ G z = G C z C
158 145 adantr φ z Y C ¬ G z = G C z C 0
159 36 42 157 46 158 dmdcan2d φ z Y C ¬ G z = G C F G z F G C G z G C G z G C z C = F G z F G C z C
160 128 130 156 159 ifbothda φ z Y C if G z = G C K F G z F G C G z G C G z G C z C = F G z F G C z C
161 fvco3 G : Y X z Y F G z = F G z
162 3 21 161 syl2an φ z Y C F G z = F G z
163 3 31 fvco3d φ F G C = F G C
164 163 adantr φ z Y C F G C = F G C
165 162 164 oveq12d φ z Y C F G z F G C = F G z F G C
166 165 oveq1d φ z Y C F G z F G C z C = F G z F G C z C
167 160 166 eqtr4d φ z Y C if G z = G C K F G z F G C G z G C G z G C z C = F G z F G C z C
168 167 mpteq2dva φ z Y C if G z = G C K F G z F G C G z G C G z G C z C = z Y C F G z F G C z C
169 168 oveq1d φ z Y C if G z = G C K F G z F G C G z G C G z G C z C lim C = z Y C F G z F G C z C lim C
170 126 169 eleqtrd φ K L z Y C F G z F G C z C lim C
171 eqid z Y C F G z F G C z C = z Y C F G z F G C z C
172 1 3 fcod φ F G : Y
173 10 9 171 6 172 4 eldv φ C F G T K L C int J 𝑡 T Y K L z Y C F G z F G C z C lim C
174 16 170 173 mpbir2and φ C F G T K L