Metamath Proof Explorer


Theorem dvaddbr

Description: The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Remove unnecessary hypotheses. (Revised by GG, 10-Apr-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 dvaddbr φ C F + f G S K + L

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 inss1 X Y X
33 ssdif X Y X X Y C X C
34 32 33 mp1i φ X Y C X C
35 34 sselda φ z X Y C z X C
36 2 5 sstrd φ X
37 28 ntrss2 J 𝑡 S Top X J 𝑡 S int J 𝑡 S X X
38 23 26 37 syl2anc φ int J 𝑡 S X X
39 38 13 sseldd φ C X
40 1 36 39 dvlem φ z X C F z F C z C
41 35 40 syldan φ z X Y C F z F C z C
42 inss2 X Y Y
43 ssdif X Y Y X Y C Y C
44 42 43 mp1i φ X Y C Y C
45 44 sselda φ z X Y C z Y C
46 4 5 sstrd φ Y
47 28 ntrss2 J 𝑡 S Top Y J 𝑡 S int J 𝑡 S Y Y
48 23 27 47 syl2anc φ int J 𝑡 S Y Y
49 48 17 sseldd φ C Y
50 3 46 49 dvlem φ z Y C G z G C z C
51 45 50 syldan φ z X Y C G z G C z C
52 ssidd φ
53 txtopon J TopOn J TopOn J × t J TopOn ×
54 19 19 53 mp2an J × t J TopOn ×
55 54 toponrestid J × t J = J × t J 𝑡 ×
56 12 simprd φ K z X C F z F C z C lim C
57 40 fmpttd φ z X C F z F C z C : X C
58 36 ssdifssd φ X C
59 eqid J 𝑡 X C C = J 𝑡 X C C
60 32 2 sstrid φ X Y S
61 60 25 sseqtrd φ X Y J 𝑡 S
62 difssd φ J 𝑡 S X J 𝑡 S
63 61 62 unssd φ X Y J 𝑡 S X J 𝑡 S
64 ssun1 X Y X Y J 𝑡 S X
65 64 a1i φ X Y X Y J 𝑡 S X
66 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
67 23 63 65 66 syl3anc φ int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S X
68 67 31 sseldd φ C int J 𝑡 S X Y J 𝑡 S X
69 68 39 elind φ C int J 𝑡 S X Y J 𝑡 S X X
70 32 a1i φ X Y X
71 eqid J 𝑡 S 𝑡 X = J 𝑡 S 𝑡 X
72 28 71 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
73 23 26 70 72 syl3anc φ int J 𝑡 S 𝑡 X X Y = int J 𝑡 S X Y J 𝑡 S X X
74 8 cnfldtop J Top
75 74 a1i φ J Top
76 cnex V
77 ssexg S V S V
78 5 76 77 sylancl φ S V
79 restabs J Top X S S V J 𝑡 S 𝑡 X = J 𝑡 X
80 75 2 78 79 syl3anc φ J 𝑡 S 𝑡 X = J 𝑡 X
81 80 fveq2d φ int J 𝑡 S 𝑡 X = int J 𝑡 X
82 81 fveq1d φ int J 𝑡 S 𝑡 X X Y = int J 𝑡 X X Y
83 73 82 eqtr3d φ int J 𝑡 S X Y J 𝑡 S X X = int J 𝑡 X X Y
84 69 83 eleqtrd φ C int J 𝑡 X X Y
85 undif1 X C C = X C
86 39 snssd φ C X
87 ssequn2 C X X C = X
88 86 87 sylib φ X C = X
89 85 88 eqtrid φ X C C = X
90 89 oveq2d φ J 𝑡 X C C = J 𝑡 X
91 90 fveq2d φ int J 𝑡 X C C = int J 𝑡 X
92 undif1 X Y C C = X Y C
93 39 49 elind φ C X Y
94 93 snssd φ C X Y
95 ssequn2 C X Y X Y C = X Y
96 94 95 sylib φ X Y C = X Y
97 92 96 eqtrid φ X Y C C = X Y
98 91 97 fveq12d φ int J 𝑡 X C C X Y C C = int J 𝑡 X X Y
99 84 98 eleqtrrd φ C int J 𝑡 X C C X Y C C
100 57 34 58 8 59 99 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
101 34 resmptd φ z X C F z F C z C X Y C = z X Y C F z F C z C
102 101 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
103 100 102 eqtr3d φ z X C F z F C z C lim C = z X Y C F z F C z C lim C
104 56 103 eleqtrd φ K z X Y C F z F C z C lim C
105 16 simprd φ L z Y C G z G C z C lim C
106 50 fmpttd φ z Y C G z G C z C : Y C
107 46 ssdifssd φ Y C
108 eqid J 𝑡 Y C C = J 𝑡 Y C C
109 difssd φ J 𝑡 S Y J 𝑡 S
110 61 109 unssd φ X Y J 𝑡 S Y J 𝑡 S
111 ssun1 X Y X Y J 𝑡 S Y
112 111 a1i φ X Y X Y J 𝑡 S Y
113 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
114 23 110 112 113 syl3anc φ int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S Y
115 114 31 sseldd φ C int J 𝑡 S X Y J 𝑡 S Y
116 115 49 elind φ C int J 𝑡 S X Y J 𝑡 S Y Y
117 42 a1i φ X Y Y
118 eqid J 𝑡 S 𝑡 Y = J 𝑡 S 𝑡 Y
119 28 118 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
120 23 27 117 119 syl3anc φ int J 𝑡 S 𝑡 Y X Y = int J 𝑡 S X Y J 𝑡 S Y Y
121 restabs J Top Y S S V J 𝑡 S 𝑡 Y = J 𝑡 Y
122 75 4 78 121 syl3anc φ J 𝑡 S 𝑡 Y = J 𝑡 Y
123 122 fveq2d φ int J 𝑡 S 𝑡 Y = int J 𝑡 Y
124 123 fveq1d φ int J 𝑡 S 𝑡 Y X Y = int J 𝑡 Y X Y
125 120 124 eqtr3d φ int J 𝑡 S X Y J 𝑡 S Y Y = int J 𝑡 Y X Y
126 116 125 eleqtrd φ C int J 𝑡 Y X Y
127 undif1 Y C C = Y C
128 49 snssd φ C Y
129 ssequn2 C Y Y C = Y
130 128 129 sylib φ Y C = Y
131 127 130 eqtrid φ Y C C = Y
132 131 oveq2d φ J 𝑡 Y C C = J 𝑡 Y
133 132 fveq2d φ int J 𝑡 Y C C = int J 𝑡 Y
134 133 97 fveq12d φ int J 𝑡 Y C C X Y C C = int J 𝑡 Y X Y
135 126 134 eleqtrrd φ C int J 𝑡 Y C C X Y C C
136 106 44 107 8 108 135 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
137 44 resmptd φ z Y C G z G C z C X Y C = z X Y C G z G C z C
138 137 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
139 136 138 eqtr3d φ z Y C G z G C z C lim C = z X Y C G z G C z C lim C
140 105 139 eleqtrd φ L z X Y C G z G C z C lim C
141 8 addcn + J × t J Cn J
142 5 1 2 dvcl φ C F S K K
143 6 142 mpdan φ K
144 5 3 4 dvcl φ C G S L L
145 7 144 mpdan φ L
146 143 145 opelxpd φ K L ×
147 54 toponunii × = J × t J
148 147 cncnpi + J × t J Cn J K L × + J × t J CnP J K L
149 141 146 148 sylancr φ + J × t J CnP J K L
150 41 51 52 52 8 55 104 140 149 limccnp2 φ K + L z X Y C F z F C z C + G z G C z C lim C
151 eldifi z X Y C z X Y
152 151 adantl φ z X Y C z X Y
153 1 ffnd φ F Fn X
154 153 adantr φ z X Y C F Fn X
155 3 ffnd φ G Fn Y
156 155 adantr φ z X Y C G Fn Y
157 ssexg X V X V
158 36 76 157 sylancl φ X V
159 158 adantr φ z X Y C X V
160 ssexg Y V Y V
161 46 76 160 sylancl φ Y V
162 161 adantr φ z X Y C Y V
163 eqid X Y = X Y
164 eqidd φ z X Y C z X F z = F z
165 eqidd φ z X Y C z Y G z = G z
166 154 156 159 162 163 164 165 ofval φ z X Y C z X Y F + f G z = F z + G z
167 152 166 mpdan φ z X Y C F + f G z = F z + G z
168 eqidd φ z X Y C C X F C = F C
169 eqidd φ z X Y C C Y G C = G C
170 154 156 159 162 163 168 169 ofval φ z X Y C C X Y F + f G C = F C + G C
171 93 170 mpidan φ z X Y C F + f G C = F C + G C
172 167 171 oveq12d φ z X Y C F + f G z F + f G C = F z + G z - F C + G C
173 difss X Y C X Y
174 173 32 sstri X Y C X
175 174 sseli z X Y C z X
176 ffvelcdm F : X z X F z
177 1 175 176 syl2an φ z X Y C F z
178 173 42 sstri X Y C Y
179 178 sseli z X Y C z Y
180 ffvelcdm G : Y z Y G z
181 3 179 180 syl2an φ z X Y C G z
182 1 39 ffvelcdmd φ F C
183 182 adantr φ z X Y C F C
184 3 49 ffvelcdmd φ G C
185 184 adantr φ z X Y C G C
186 177 181 183 185 addsub4d φ z X Y C F z + G z - F C + G C = F z F C + G z - G C
187 172 186 eqtrd φ z X Y C F + f G z F + f G C = F z F C + G z - G C
188 187 oveq1d φ z X Y C F + f G z F + f G C z C = F z F C + G z - G C z C
189 177 183 subcld φ z X Y C F z F C
190 181 185 subcld φ z X Y C G z G C
191 174 36 sstrid φ X Y C
192 191 sselda φ z X Y C z
193 36 39 sseldd φ C
194 193 adantr φ z X Y C C
195 192 194 subcld φ z X Y C z C
196 eldifsni z X Y C z C
197 196 adantl φ z X Y C z C
198 192 194 197 subne0d φ z X Y C z C 0
199 189 190 195 198 divdird φ z X Y C F z F C + G z - G C z C = F z F C z C + G z G C z C
200 188 199 eqtrd φ z X Y C F + f G z F + f G C z C = F z F C z C + G z G C z C
201 200 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 C z C
202 201 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 C z C lim C
203 150 202 eleqtrrd φ K + L z X Y C F + f G z F + f G C z C lim C
204 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
205 addcl x y x + y
206 205 adantl φ x y x + y
207 206 1 3 158 161 163 off φ F + f G : X Y
208 9 8 204 5 207 60 eldv φ C F + f G S K + L C int J 𝑡 S X Y K + L z X Y C F + f G z F + f G C z C lim C
209 31 203 208 mpbir2and φ C F + f G S K + L