Metamath Proof Explorer


Theorem dvmulbrOLD

Description: Obsolete version of dvmulbr as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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 dvmulbrOLD φ 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 91 31 sseldd φ C int J 𝑡 S X Y J 𝑡 S X
93 92 42 elind φ C int J 𝑡 S X Y J 𝑡 S X X
94 33 a1i φ X Y X
95 eqid J 𝑡 S 𝑡 X = J 𝑡 S 𝑡 X
96 28 95 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
97 23 26 94 96 syl3anc φ int J 𝑡 S 𝑡 X X Y = int J 𝑡 S X Y J 𝑡 S X X
98 8 cnfldtop J Top
99 98 a1i φ J Top
100 cnex V
101 ssexg S V S V
102 5 100 101 sylancl φ S V
103 restabs J Top X S S V J 𝑡 S 𝑡 X = J 𝑡 X
104 99 2 102 103 syl3anc φ J 𝑡 S 𝑡 X = J 𝑡 X
105 104 fveq2d φ int J 𝑡 S 𝑡 X = int J 𝑡 X
106 105 fveq1d φ int J 𝑡 S 𝑡 X X Y = int J 𝑡 X X Y
107 97 106 eqtr3d φ int J 𝑡 S X Y J 𝑡 S X X = int J 𝑡 X X Y
108 93 107 eleqtrd φ C int J 𝑡 X X Y
109 undif1 X C C = X C
110 42 snssd φ C X
111 ssequn2 C X X C = X
112 110 111 sylib φ X C = X
113 109 112 eqtrid φ X C C = X
114 113 oveq2d φ J 𝑡 X C C = J 𝑡 X
115 114 fveq2d φ int J 𝑡 X C C = int J 𝑡 X
116 undif1 X Y C C = X Y C
117 42 69 elind φ C X Y
118 117 snssd φ C X Y
119 ssequn2 C X Y X Y C = X Y
120 118 119 sylib φ X Y C = X Y
121 116 120 eqtrid φ X Y C C = X Y
122 115 121 fveq12d φ int J 𝑡 X C C X Y C C = int J 𝑡 X X Y
123 108 122 eleqtrrd φ C int J 𝑡 X C C X Y C C
124 79 81 82 8 83 123 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
125 81 resmptd φ z X C F z F C z C X Y C = z X Y C F z F C z C
126 125 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
127 124 126 eqtr3d φ z X C F z F C z C lim C = z X Y C F z F C z C lim C
128 77 127 eleqtrd φ K z X Y C F z F C z C lim C
129 eqid J 𝑡 Y = J 𝑡 Y
130 129 8 dvcnp2 S G : Y Y S C dom G S G J 𝑡 Y CnP J C
131 5 3 4 68 130 syl31anc φ G J 𝑡 Y CnP J C
132 8 129 cnplimc Y C Y G J 𝑡 Y CnP J C G : Y G C G lim C
133 64 69 132 syl2anc φ G J 𝑡 Y CnP J C G : Y G C G lim C
134 131 133 mpbid φ G : Y G C G lim C
135 134 simprd φ G C G lim C
136 difss X Y C X Y
137 136 57 sstri X Y C Y
138 137 a1i φ X Y C Y
139 eqid J 𝑡 Y C = J 𝑡 Y C
140 difssd φ J 𝑡 S Y J 𝑡 S
141 85 140 unssd φ X Y J 𝑡 S Y J 𝑡 S
142 ssun1 X Y X Y J 𝑡 S Y
143 142 a1i φ X Y X Y J 𝑡 S Y
144 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
145 23 141 143 144 syl3anc φ int J 𝑡 S X Y int J 𝑡 S X Y J 𝑡 S Y
146 145 31 sseldd φ C int J 𝑡 S X Y J 𝑡 S Y
147 146 69 elind φ C int J 𝑡 S X Y J 𝑡 S Y Y
148 57 a1i φ X Y Y
149 eqid J 𝑡 S 𝑡 Y = J 𝑡 S 𝑡 Y
150 28 149 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
151 23 27 148 150 syl3anc φ int J 𝑡 S 𝑡 Y X Y = int J 𝑡 S X Y J 𝑡 S Y Y
152 restabs J Top Y S S V J 𝑡 S 𝑡 Y = J 𝑡 Y
153 99 4 102 152 syl3anc φ J 𝑡 S 𝑡 Y = J 𝑡 Y
154 153 fveq2d φ int J 𝑡 S 𝑡 Y = int J 𝑡 Y
155 154 fveq1d φ int J 𝑡 S 𝑡 Y X Y = int J 𝑡 Y X Y
156 151 155 eqtr3d φ int J 𝑡 S X Y J 𝑡 S Y Y = int J 𝑡 Y X Y
157 147 156 eleqtrd φ C int J 𝑡 Y X Y
158 69 snssd φ C Y
159 ssequn2 C Y Y C = Y
160 158 159 sylib φ Y C = Y
161 160 oveq2d φ J 𝑡 Y C = J 𝑡 Y
162 161 fveq2d φ int J 𝑡 Y C = int J 𝑡 Y
163 162 121 fveq12d φ int J 𝑡 Y C X Y C C = int J 𝑡 Y X Y
164 157 163 eleqtrrd φ C int J 𝑡 Y C X Y C C
165 3 138 64 8 139 164 limcres φ G X Y C lim C = G lim C
166 3 138 feqresmpt φ G X Y C = z X Y C G z
167 166 oveq1d φ G X Y C lim C = z X Y C G z lim C
168 165 167 eqtr3d φ G lim C = z X Y C G z lim C
169 135 168 eleqtrd φ G C z X Y C G z lim C
170 8 mulcn × J × t J Cn J
171 5 1 2 dvcl φ C F S K K
172 6 171 mpdan φ K
173 3 69 ffvelcdmd φ G C
174 172 173 opelxpd φ K G C ×
175 75 toponunii × = J × t J
176 175 cncnpi × J × t J Cn J K G C × × J × t J CnP J K G C
177 170 174 176 sylancr φ × J × t J CnP J K G C
178 55 59 73 73 8 76 128 169 177 limccnp2 φ K G C z X Y C F z F C z C G z lim C
179 16 simprd φ L z Y C G z G C z C lim C
180 70 fmpttd φ z Y C G z G C z C : Y C
181 64 ssdifssd φ Y C
182 eqid J 𝑡 Y C C = J 𝑡 Y C C
183 undif1 Y C C = Y C
184 183 160 eqtrid φ Y C C = Y
185 184 oveq2d φ J 𝑡 Y C C = J 𝑡 Y
186 185 fveq2d φ int J 𝑡 Y C C = int J 𝑡 Y
187 186 121 fveq12d φ int J 𝑡 Y C C X Y C C = int J 𝑡 Y X Y
188 157 187 eleqtrrd φ C int J 𝑡 Y C C X Y C C
189 180 62 181 8 182 188 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
190 62 resmptd φ z Y C G z G C z C X Y C = z X Y C G z G C z C
191 190 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
192 189 191 eqtr3d φ z Y C G z G C z C lim C = z X Y C G z G C z C lim C
193 179 192 eleqtrd φ L z X Y C G z G C z C lim C
194 84 5 sstrd φ X Y
195 cncfmptc F C X Y z X Y F C : X Y cn
196 43 194 73 195 syl3anc φ z X Y F C : X Y cn
197 eqidd z = C F C = F C
198 196 117 197 cnmptlimc φ F C z X Y F C lim C
199 43 adantr φ z X Y F C
200 199 fmpttd φ z X Y F C : X Y
201 200 limcdif φ z X Y F C lim C = z X Y F C X Y C lim C
202 resmpt X Y C X Y z X Y F C X Y C = z X Y C F C
203 136 202 mp1i φ z X Y F C X Y C = z X Y C F C
204 203 oveq1d φ z X Y F C X Y C lim C = z X Y C F C lim C
205 201 204 eqtrd φ z X Y F C lim C = z X Y C F C lim C
206 198 205 eleqtrd φ F C z X Y C F C lim C
207 5 3 4 dvcl φ C G S L L
208 7 207 mpdan φ L
209 208 43 opelxpd φ L F C ×
210 175 cncnpi × J × t J Cn J L F C × × J × t J CnP J L F C
211 170 209 210 sylancr φ × J × t J CnP J L F C
212 71 44 73 73 8 76 193 206 211 limccnp2 φ L F C z X Y C G z G C z C F C lim C
213 8 addcn + J × t J Cn J
214 172 173 mulcld φ K G C
215 208 43 mulcld φ L F C
216 214 215 opelxpd φ K G C L F C ×
217 175 cncnpi + J × t J Cn J K G C L F C × + J × t J CnP J K G C L F C
218 213 216 217 sylancr φ + J × t J CnP J K G C L F C
219 60 72 73 73 8 76 178 212 218 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
220 42 adantr φ z X Y C C X
221 32 220 ffvelcdmd φ z X Y C F C
222 37 221 subcld φ z X Y C F z F C
223 222 59 mulcld φ z X Y C F z F C G z
224 69 adantr φ z X Y C C Y
225 56 224 ffvelcdmd φ z X Y C G C
226 59 225 subcld φ z X Y C G z G C
227 226 221 mulcld φ z X Y C G z G C F C
228 47 220 sseldd φ z X Y C C
229 48 228 subcld φ z X Y C z C
230 223 227 229 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
231 37 59 mulcld φ z X Y C F z G z
232 221 59 mulcld φ z X Y C F C G z
233 221 225 mulcld φ z X Y C F C G C
234 231 232 233 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
235 37 221 59 subdird φ z X Y C F z F C G z = F z G z F C G z
236 226 221 mulcomd φ z X Y C G z G C F C = F C G z G C
237 221 59 225 subdid φ z X Y C F C G z G C = F C G z F C G C
238 236 237 eqtrd φ z X Y C G z G C F C = F C G z F C G C
239 235 238 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
240 1 ffnd φ F Fn X
241 240 adantr φ z X Y C F Fn X
242 3 ffnd φ G Fn Y
243 242 adantr φ z X Y C G Fn Y
244 ssexg X V X V
245 46 100 244 sylancl φ X V
246 245 adantr φ z X Y C X V
247 ssexg Y V Y V
248 64 100 247 sylancl φ Y V
249 248 adantr φ z X Y C Y V
250 eqid X Y = X Y
251 eqidd φ z X Y C z X F z = F z
252 eqidd φ z X Y C z Y G z = G z
253 241 243 246 249 250 251 252 ofval φ z X Y C z X Y F × f G z = F z G z
254 35 253 mpdan φ z X Y C F × f G z = F z G z
255 eqidd φ z X Y C C X F C = F C
256 eqidd φ z X Y C C Y G C = G C
257 241 243 246 249 250 255 256 ofval φ z X Y C C X Y F × f G C = F C G C
258 117 257 mpidan φ z X Y C F × f G C = F C G C
259 254 258 oveq12d φ z X Y C F × f G z F × f G C = F z G z F C G C
260 234 239 259 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
261 260 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
262 222 59 229 54 div23d φ z X Y C F z F C G z z C = F z F C z C G z
263 226 221 229 54 div23d φ z X Y C G z G C F C z C = G z G C z C F C
264 262 263 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
265 230 261 264 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
266 265 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
267 266 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
268 219 267 eleqtrrd φ K G C + L F C z X Y C F × f G z F × f G C z C lim C
269 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
270 mulcl x y x y
271 270 adantl φ x y x y
272 271 1 3 245 248 250 off φ F × f G : X Y
273 9 8 269 5 272 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
274 31 268 273 mpbir2and φ C F × f G S K G C + L F C