Metamath Proof Explorer


Theorem cncfiooicclem1

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B . F can be complex-valued. This lemma assumes A < B , the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfiooicclem1.x x φ
cncfiooicclem1.g G = x A B if x = A R if x = B L F x
cncfiooicclem1.a φ A
cncfiooicclem1.b φ B
cncfiooicclem1.altb φ A < B
cncfiooicclem1.f φ F : A B cn
cncfiooicclem1.l φ L F lim B
cncfiooicclem1.r φ R F lim A
Assertion cncfiooicclem1 φ G : A B cn

Proof

Step Hyp Ref Expression
1 cncfiooicclem1.x x φ
2 cncfiooicclem1.g G = x A B if x = A R if x = B L F x
3 cncfiooicclem1.a φ A
4 cncfiooicclem1.b φ B
5 cncfiooicclem1.altb φ A < B
6 cncfiooicclem1.f φ F : A B cn
7 cncfiooicclem1.l φ L F lim B
8 cncfiooicclem1.r φ R F lim A
9 limccl F lim A
10 9 8 sseldi φ R
11 10 ad2antrr φ x A B x = A R
12 limccl F lim B
13 12 7 sseldi φ L
14 13 ad3antrrr φ x A B ¬ x = A x = B L
15 simplll φ x A B ¬ x = A ¬ x = B φ
16 orel1 ¬ x = A x = A x = B x = B
17 16 con3dimp ¬ x = A ¬ x = B ¬ x = A x = B
18 vex x V
19 18 elpr x A B x = A x = B
20 17 19 sylnibr ¬ x = A ¬ x = B ¬ x A B
21 20 adantll φ x A B ¬ x = A ¬ x = B ¬ x A B
22 simpllr φ x A B ¬ x = A ¬ x = B x A B
23 3 rexrd φ A *
24 15 23 syl φ x A B ¬ x = A ¬ x = B A *
25 4 rexrd φ B *
26 15 25 syl φ x A B ¬ x = A ¬ x = B B *
27 3 4 5 ltled φ A B
28 15 27 syl φ x A B ¬ x = A ¬ x = B A B
29 prunioo A * B * A B A B A B = A B
30 24 26 28 29 syl3anc φ x A B ¬ x = A ¬ x = B A B A B = A B
31 22 30 eleqtrrd φ x A B ¬ x = A ¬ x = B x A B A B
32 elun x A B A B x A B x A B
33 31 32 sylib φ x A B ¬ x = A ¬ x = B x A B x A B
34 orel2 ¬ x A B x A B x A B x A B
35 21 33 34 sylc φ x A B ¬ x = A ¬ x = B x A B
36 cncff F : A B cn F : A B
37 6 36 syl φ F : A B
38 37 ffvelrnda φ x A B F x
39 15 35 38 syl2anc φ x A B ¬ x = A ¬ x = B F x
40 14 39 ifclda φ x A B ¬ x = A if x = B L F x
41 11 40 ifclda φ x A B if x = A R if x = B L F x
42 1 41 2 fmptdf φ G : A B
43 elun y A B A B y A B y A B
44 23 25 27 29 syl3anc φ A B A B = A B
45 44 eleq2d φ y A B A B y A B
46 43 45 bitr3id φ y A B y A B y A B
47 46 biimpar φ y A B y A B y A B
48 ioossicc A B A B
49 fssres G : A B A B A B G A B : A B
50 42 48 49 sylancl φ G A B : A B
51 50 feqmptd φ G A B = y A B G A B y
52 nfmpt1 _ x x A B if x = A R if x = B L F x
53 2 52 nfcxfr _ x G
54 nfcv _ x A B
55 53 54 nfres _ x G A B
56 nfcv _ x y
57 55 56 nffv _ x G A B y
58 nfcv _ y G A B
59 nfcv _ y x
60 58 59 nffv _ y G A B x
61 fveq2 y = x G A B y = G A B x
62 57 60 61 cbvmpt y A B G A B y = x A B G A B x
63 62 a1i φ y A B G A B y = x A B G A B x
64 fvres x A B G A B x = G x
65 64 adantl φ x A B G A B x = G x
66 simpr φ x A B x A B
67 48 66 sseldi φ x A B x A B
68 10 adantr φ x A B R
69 13 ad2antrr φ x A B x = B L
70 38 adantr φ x A B ¬ x = B F x
71 69 70 ifclda φ x A B if x = B L F x
72 68 71 ifcld φ x A B if x = A R if x = B L F x
73 2 fvmpt2 x A B if x = A R if x = B L F x G x = if x = A R if x = B L F x
74 67 72 73 syl2anc φ x A B G x = if x = A R if x = B L F x
75 elioo4g x A B A * B * x A < x x < B
76 75 biimpi x A B A * B * x A < x x < B
77 76 simpld x A B A * B * x
78 77 simp1d x A B A *
79 elioore x A B x
80 79 rexrd x A B x *
81 eliooord x A B A < x x < B
82 81 simpld x A B A < x
83 xrltne A * x * A < x x A
84 78 80 82 83 syl3anc x A B x A
85 84 adantl φ x A B x A
86 85 neneqd φ x A B ¬ x = A
87 86 iffalsed φ x A B if x = A R if x = B L F x = if x = B L F x
88 81 simprd x A B x < B
89 79 88 ltned x A B x B
90 89 neneqd x A B ¬ x = B
91 90 iffalsed x A B if x = B L F x = F x
92 91 adantl φ x A B if x = B L F x = F x
93 87 92 eqtrd φ x A B if x = A R if x = B L F x = F x
94 65 74 93 3eqtrd φ x A B G A B x = F x
95 1 94 mpteq2da φ x A B G A B x = x A B F x
96 51 63 95 3eqtrd φ G A B = x A B F x
97 37 feqmptd φ F = x A B F x
98 ioosscn A B
99 98 a1i φ A B
100 ssid
101 eqid TopOpen fld = TopOpen fld
102 eqid TopOpen fld 𝑡 A B = TopOpen fld 𝑡 A B
103 101 cnfldtop TopOpen fld Top
104 unicntop = TopOpen fld
105 104 restid TopOpen fld Top TopOpen fld 𝑡 = TopOpen fld
106 103 105 ax-mp TopOpen fld 𝑡 = TopOpen fld
107 106 eqcomi TopOpen fld = TopOpen fld 𝑡
108 101 102 107 cncfcn A B A B cn = TopOpen fld 𝑡 A B Cn TopOpen fld
109 99 100 108 sylancl φ A B cn = TopOpen fld 𝑡 A B Cn TopOpen fld
110 6 97 109 3eltr3d φ x A B F x TopOpen fld 𝑡 A B Cn TopOpen fld
111 96 110 eqeltrd φ G A B TopOpen fld 𝑡 A B Cn TopOpen fld
112 104 restuni TopOpen fld Top A B A B = TopOpen fld 𝑡 A B
113 103 98 112 mp2an A B = TopOpen fld 𝑡 A B
114 113 cncnpi G A B TopOpen fld 𝑡 A B Cn TopOpen fld y A B G A B TopOpen fld 𝑡 A B CnP TopOpen fld y
115 111 114 sylan φ y A B G A B TopOpen fld 𝑡 A B CnP TopOpen fld y
116 103 a1i φ y A B TopOpen fld Top
117 48 a1i φ y A B A B A B
118 ovex A B V
119 118 a1i φ y A B A B V
120 restabs TopOpen fld Top A B A B A B V TopOpen fld 𝑡 A B 𝑡 A B = TopOpen fld 𝑡 A B
121 116 117 119 120 syl3anc φ y A B TopOpen fld 𝑡 A B 𝑡 A B = TopOpen fld 𝑡 A B
122 121 eqcomd φ y A B TopOpen fld 𝑡 A B = TopOpen fld 𝑡 A B 𝑡 A B
123 122 oveq1d φ y A B TopOpen fld 𝑡 A B CnP TopOpen fld = TopOpen fld 𝑡 A B 𝑡 A B CnP TopOpen fld
124 123 fveq1d φ y A B TopOpen fld 𝑡 A B CnP TopOpen fld y = TopOpen fld 𝑡 A B 𝑡 A B CnP TopOpen fld y
125 115 124 eleqtrd φ y A B G A B TopOpen fld 𝑡 A B 𝑡 A B CnP TopOpen fld y
126 resttop TopOpen fld Top A B V TopOpen fld 𝑡 A B Top
127 103 118 126 mp2an TopOpen fld 𝑡 A B Top
128 127 a1i φ y A B TopOpen fld 𝑡 A B Top
129 48 a1i φ A B A B
130 3 4 iccssred φ A B
131 ax-resscn
132 130 131 sstrdi φ A B
133 104 restuni TopOpen fld Top A B A B = TopOpen fld 𝑡 A B
134 103 132 133 sylancr φ A B = TopOpen fld 𝑡 A B
135 129 134 sseqtrd φ A B TopOpen fld 𝑡 A B
136 135 adantr φ y A B A B TopOpen fld 𝑡 A B
137 retop topGen ran . Top
138 137 a1i φ y A B topGen ran . Top
139 ioossre A B
140 difss A B
141 139 140 unssi A B A B
142 141 a1i φ y A B A B A B
143 ssun1 A B A B A B
144 143 a1i φ y A B A B A B A B
145 uniretop = topGen ran .
146 145 ntrss topGen ran . Top A B A B A B A B A B int topGen ran . A B int topGen ran . A B A B
147 138 142 144 146 syl3anc φ y A B int topGen ran . A B int topGen ran . A B A B
148 simpr φ y A B y A B
149 ioontr int topGen ran . A B = A B
150 148 149 eleqtrrdi φ y A B y int topGen ran . A B
151 147 150 sseldd φ y A B y int topGen ran . A B A B
152 48 148 sseldi φ y A B y A B
153 151 152 elind φ y A B y int topGen ran . A B A B A B
154 130 adantr φ y A B A B
155 eqid topGen ran . 𝑡 A B = topGen ran . 𝑡 A B
156 145 155 restntr topGen ran . Top A B A B A B int topGen ran . 𝑡 A B A B = int topGen ran . A B A B A B
157 138 154 117 156 syl3anc φ y A B int topGen ran . 𝑡 A B A B = int topGen ran . A B A B A B
158 153 157 eleqtrrd φ y A B y int topGen ran . 𝑡 A B A B
159 101 tgioo2 topGen ran . = TopOpen fld 𝑡
160 159 a1i φ topGen ran . = TopOpen fld 𝑡
161 160 oveq1d φ topGen ran . 𝑡 A B = TopOpen fld 𝑡 𝑡 A B
162 103 a1i φ TopOpen fld Top
163 reex V
164 163 a1i φ V
165 restabs TopOpen fld Top A B V TopOpen fld 𝑡 𝑡 A B = TopOpen fld 𝑡 A B
166 162 130 164 165 syl3anc φ TopOpen fld 𝑡 𝑡 A B = TopOpen fld 𝑡 A B
167 161 166 eqtrd φ topGen ran . 𝑡 A B = TopOpen fld 𝑡 A B
168 167 fveq2d φ int topGen ran . 𝑡 A B = int TopOpen fld 𝑡 A B
169 168 fveq1d φ int topGen ran . 𝑡 A B A B = int TopOpen fld 𝑡 A B A B
170 169 adantr φ y A B int topGen ran . 𝑡 A B A B = int TopOpen fld 𝑡 A B A B
171 158 170 eleqtrd φ y A B y int TopOpen fld 𝑡 A B A B
172 134 feq2d φ G : A B G : TopOpen fld 𝑡 A B
173 42 172 mpbid φ G : TopOpen fld 𝑡 A B
174 173 adantr φ y A B G : TopOpen fld 𝑡 A B
175 eqid TopOpen fld 𝑡 A B = TopOpen fld 𝑡 A B
176 175 104 cnprest TopOpen fld 𝑡 A B Top A B TopOpen fld 𝑡 A B y int TopOpen fld 𝑡 A B A B G : TopOpen fld 𝑡 A B G TopOpen fld 𝑡 A B CnP TopOpen fld y G A B TopOpen fld 𝑡 A B 𝑡 A B CnP TopOpen fld y
177 128 136 171 174 176 syl22anc φ y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y G A B TopOpen fld 𝑡 A B 𝑡 A B CnP TopOpen fld y
178 125 177 mpbird φ y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
179 elpri y A B y = A y = B
180 iftrue x = A if x = A R if x = B L F x = R
181 lbicc2 A * B * A B A A B
182 23 25 27 181 syl3anc φ A A B
183 2 180 182 8 fvmptd3 φ G A = R
184 97 eqcomd φ x A B F x = F
185 96 184 eqtr2d φ F = G A B
186 185 oveq1d φ F lim A = G A B lim A
187 8 186 eleqtrd φ R G A B lim A
188 3 4 5 42 limciccioolb φ G A B lim A = G lim A
189 187 188 eleqtrd φ R G lim A
190 183 189 eqeltrd φ G A G lim A
191 eqid TopOpen fld 𝑡 A B = TopOpen fld 𝑡 A B
192 101 191 cnplimc A B A A B G TopOpen fld 𝑡 A B CnP TopOpen fld A G : A B G A G lim A
193 132 182 192 syl2anc φ G TopOpen fld 𝑡 A B CnP TopOpen fld A G : A B G A G lim A
194 42 190 193 mpbir2and φ G TopOpen fld 𝑡 A B CnP TopOpen fld A
195 194 adantr φ y = A G TopOpen fld 𝑡 A B CnP TopOpen fld A
196 fveq2 y = A TopOpen fld 𝑡 A B CnP TopOpen fld y = TopOpen fld 𝑡 A B CnP TopOpen fld A
197 196 eqcomd y = A TopOpen fld 𝑡 A B CnP TopOpen fld A = TopOpen fld 𝑡 A B CnP TopOpen fld y
198 197 adantl φ y = A TopOpen fld 𝑡 A B CnP TopOpen fld A = TopOpen fld 𝑡 A B CnP TopOpen fld y
199 195 198 eleqtrd φ y = A G TopOpen fld 𝑡 A B CnP TopOpen fld y
200 180 adantl x = B x = A if x = A R if x = B L F x = R
201 eqtr2 x = B x = A B = A
202 iftrue B = A if B = A R if B = B L F B = R
203 202 eqcomd B = A R = if B = A R if B = B L F B
204 201 203 syl x = B x = A R = if B = A R if B = B L F B
205 200 204 eqtrd x = B x = A if x = A R if x = B L F x = if B = A R if B = B L F B
206 iffalse ¬ x = A if x = A R if x = B L F x = if x = B L F x
207 206 adantl x = B ¬ x = A if x = A R if x = B L F x = if x = B L F x
208 iftrue x = B if x = B L F x = L
209 208 adantr x = B ¬ x = A if x = B L F x = L
210 df-ne x A ¬ x = A
211 pm13.18 x = B x A B A
212 210 211 sylan2br x = B ¬ x = A B A
213 212 neneqd x = B ¬ x = A ¬ B = A
214 213 iffalsed x = B ¬ x = A if B = A R if B = B L F B = if B = B L F B
215 eqid B = B
216 215 iftruei if B = B L F B = L
217 214 216 eqtr2di x = B ¬ x = A L = if B = A R if B = B L F B
218 207 209 217 3eqtrd x = B ¬ x = A if x = A R if x = B L F x = if B = A R if B = B L F B
219 205 218 pm2.61dan x = B if x = A R if x = B L F x = if B = A R if B = B L F B
220 4 leidd φ B B
221 3 4 4 27 220 eliccd φ B A B
222 216 13 eqeltrid φ if B = B L F B
223 10 222 ifcld φ if B = A R if B = B L F B
224 2 219 221 223 fvmptd3 φ G B = if B = A R if B = B L F B
225 3 5 gtned φ B A
226 225 neneqd φ ¬ B = A
227 226 iffalsed φ if B = A R if B = B L F B = if B = B L F B
228 216 a1i φ if B = B L F B = L
229 224 227 228 3eqtrd φ G B = L
230 185 oveq1d φ F lim B = G A B lim B
231 7 230 eleqtrd φ L G A B lim B
232 3 4 5 42 limcicciooub φ G A B lim B = G lim B
233 231 232 eleqtrd φ L G lim B
234 229 233 eqeltrd φ G B G lim B
235 101 191 cnplimc A B B A B G TopOpen fld 𝑡 A B CnP TopOpen fld B G : A B G B G lim B
236 132 221 235 syl2anc φ G TopOpen fld 𝑡 A B CnP TopOpen fld B G : A B G B G lim B
237 42 234 236 mpbir2and φ G TopOpen fld 𝑡 A B CnP TopOpen fld B
238 237 adantr φ y = B G TopOpen fld 𝑡 A B CnP TopOpen fld B
239 fveq2 y = B TopOpen fld 𝑡 A B CnP TopOpen fld y = TopOpen fld 𝑡 A B CnP TopOpen fld B
240 239 eqcomd y = B TopOpen fld 𝑡 A B CnP TopOpen fld B = TopOpen fld 𝑡 A B CnP TopOpen fld y
241 240 adantl φ y = B TopOpen fld 𝑡 A B CnP TopOpen fld B = TopOpen fld 𝑡 A B CnP TopOpen fld y
242 238 241 eleqtrd φ y = B G TopOpen fld 𝑡 A B CnP TopOpen fld y
243 199 242 jaodan φ y = A y = B G TopOpen fld 𝑡 A B CnP TopOpen fld y
244 179 243 sylan2 φ y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
245 178 244 jaodan φ y A B y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
246 47 245 syldan φ y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
247 246 ralrimiva φ y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
248 101 cnfldtopon TopOpen fld TopOn
249 resttopon TopOpen fld TopOn A B TopOpen fld 𝑡 A B TopOn A B
250 248 132 249 sylancr φ TopOpen fld 𝑡 A B TopOn A B
251 cncnp TopOpen fld 𝑡 A B TopOn A B TopOpen fld TopOn G TopOpen fld 𝑡 A B Cn TopOpen fld G : A B y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
252 250 248 251 sylancl φ G TopOpen fld 𝑡 A B Cn TopOpen fld G : A B y A B G TopOpen fld 𝑡 A B CnP TopOpen fld y
253 42 247 252 mpbir2and φ G TopOpen fld 𝑡 A B Cn TopOpen fld
254 101 191 107 cncfcn A B A B cn = TopOpen fld 𝑡 A B Cn TopOpen fld
255 132 100 254 sylancl φ A B cn = TopOpen fld 𝑡 A B Cn TopOpen fld
256 253 255 eleqtrrd φ G : A B cn