Metamath Proof Explorer

Theorem cncfiooicc

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. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfiooicc.x 
|- F/ x ph
cncfiooicc.g 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
cncfiooicc.a 
|- ( ph -> A e. RR )
cncfiooicc.b 
|- ( ph -> B e. RR )
cncfiooicc.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
cncfiooicc.l 
|- ( ph -> L e. ( F limCC B ) )
cncfiooicc.r 
|- ( ph -> R e. ( F limCC A ) )
Assertion cncfiooicc 
|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cncfiooicc.x 
 |-  F/ x ph
2 cncfiooicc.g 
 |-  G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
3 cncfiooicc.a 
 |-  ( ph -> A e. RR )
4 cncfiooicc.b 
 |-  ( ph -> B e. RR )
5 cncfiooicc.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
6 cncfiooicc.l 
 |-  ( ph -> L e. ( F limCC B ) )
7 cncfiooicc.r 
 |-  ( ph -> R e. ( F limCC A ) )
8 nfv 
 |-  F/ x ( ph /\ A < B )
9 3 adantr 
 |-  ( ( ph /\ A < B ) -> A e. RR )
10 4 adantr 
 |-  ( ( ph /\ A < B ) -> B e. RR )
11 simpr 
 |-  ( ( ph /\ A < B ) -> A < B )
12 5 adantr 
 |-  ( ( ph /\ A < B ) -> F e. ( ( A (,) B ) -cn-> CC ) )
13 6 adantr 
 |-  ( ( ph /\ A < B ) -> L e. ( F limCC B ) )
14 7 adantr 
 |-  ( ( ph /\ A < B ) -> R e. ( F limCC A ) )
15 8 2 9 10 11 12 13 14 cncfiooicclem1 
 |-  ( ( ph /\ A < B ) -> G e. ( ( A [,] B ) -cn-> CC ) )
16 limccl 
 |-  ( F limCC A ) C_ CC
17 16 7 sseldi 
 |-  ( ph -> R e. CC )
18 17 snssd 
 |-  ( ph -> { R } C_ CC )
19 ssid 
 |-  CC C_ CC
20 19 a1i 
 |-  ( ph -> CC C_ CC )
21 cncfss 
 |-  ( ( { R } C_ CC /\ CC C_ CC ) -> ( { A } -cn-> { R } ) C_ ( { A } -cn-> CC ) )
22 18 20 21 syl2anc 
 |-  ( ph -> ( { A } -cn-> { R } ) C_ ( { A } -cn-> CC ) )
23 22 adantr 
 |-  ( ( ph /\ A = B ) -> ( { A } -cn-> { R } ) C_ ( { A } -cn-> CC ) )
24 3 rexrd 
 |-  ( ph -> A e. RR* )
25 iccid 
 |-  ( A e. RR* -> ( A [,] A ) = { A } )
26 24 25 syl 
 |-  ( ph -> ( A [,] A ) = { A } )
27 oveq2 
 |-  ( A = B -> ( A [,] A ) = ( A [,] B ) )
28 26 27 sylan9req 
 |-  ( ( ph /\ A = B ) -> { A } = ( A [,] B ) )
29 28 eqcomd 
 |-  ( ( ph /\ A = B ) -> ( A [,] B ) = { A } )
30 simpr 
 |-  ( ( ( ph /\ A = B ) /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
31 29 adantr 
 |-  ( ( ( ph /\ A = B ) /\ x e. ( A [,] B ) ) -> ( A [,] B ) = { A } )
32 30 31 eleqtrd 
 |-  ( ( ( ph /\ A = B ) /\ x e. ( A [,] B ) ) -> x e. { A } )
33 elsni 
 |-  ( x e. { A } -> x = A )
34 32 33 syl 
 |-  ( ( ( ph /\ A = B ) /\ x e. ( A [,] B ) ) -> x = A )
35 34 iftrued 
 |-  ( ( ( ph /\ A = B ) /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
36 29 35 mpteq12dva 
 |-  ( ( ph /\ A = B ) -> ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) = ( x e. { A } |-> R ) )
37 2 36 syl5eq 
 |-  ( ( ph /\ A = B ) -> G = ( x e. { A } |-> R ) )
38 3 recnd 
 |-  ( ph -> A e. CC )
39 38 adantr 
 |-  ( ( ph /\ A = B ) -> A e. CC )
40 17 adantr 
 |-  ( ( ph /\ A = B ) -> R e. CC )
41 cncfdmsn 
 |-  ( ( A e. CC /\ R e. CC ) -> ( x e. { A } |-> R ) e. ( { A } -cn-> { R } ) )
42 39 40 41 syl2anc 
 |-  ( ( ph /\ A = B ) -> ( x e. { A } |-> R ) e. ( { A } -cn-> { R } ) )
43 37 42 eqeltrd 
 |-  ( ( ph /\ A = B ) -> G e. ( { A } -cn-> { R } ) )
44 23 43 sseldd 
 |-  ( ( ph /\ A = B ) -> G e. ( { A } -cn-> CC ) )
45 28 oveq1d 
 |-  ( ( ph /\ A = B ) -> ( { A } -cn-> CC ) = ( ( A [,] B ) -cn-> CC ) )
46 44 45 eleqtrd 
 |-  ( ( ph /\ A = B ) -> G e. ( ( A [,] B ) -cn-> CC ) )
47 46 adantlr 
 |-  ( ( ( ph /\ -. A < B ) /\ A = B ) -> G e. ( ( A [,] B ) -cn-> CC ) )
48 simpll 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> ph )
49 eqcom 
 |-  ( B = A <-> A = B )
50 49 biimpi 
 |-  ( B = A -> A = B )
51 50 con3i 
 |-  ( -. A = B -> -. B = A )
52 51 adantl 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> -. B = A )
53 simplr 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> -. A < B )
54 pm4.56 
 |-  ( ( -. B = A /\ -. A < B ) <-> -. ( B = A \/ A < B ) )
55 54 biimpi 
 |-  ( ( -. B = A /\ -. A < B ) -> -. ( B = A \/ A < B ) )
56 52 53 55 syl2anc 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> -. ( B = A \/ A < B ) )
57 48 4 syl 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> B e. RR )
58 48 3 syl 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> A e. RR )
59 57 58 lttrid 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> ( B < A <-> -. ( B = A \/ A < B ) ) )
60 56 59 mpbird 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> B < A )
61 0ss 
 |-  (/) C_ CC
62 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
63 62 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
64 rest0 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t (/) ) = { (/) } )
65 63 64 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t (/) ) = { (/) }
66 65 eqcomi 
 |-  { (/) } = ( ( TopOpen ` CCfld ) |`t (/) )
67 62 66 66 cncfcn 
 |-  ( ( (/) C_ CC /\ (/) C_ CC ) -> ( (/) -cn-> (/) ) = ( { (/) } Cn { (/) } ) )
68 61 61 67 mp2an 
 |-  ( (/) -cn-> (/) ) = ( { (/) } Cn { (/) } )
69 cncfss 
 |-  ( ( (/) C_ CC /\ CC C_ CC ) -> ( (/) -cn-> (/) ) C_ ( (/) -cn-> CC ) )
70 61 19 69 mp2an 
 |-  ( (/) -cn-> (/) ) C_ ( (/) -cn-> CC )
71 68 70 eqsstrri 
 |-  ( { (/) } Cn { (/) } ) C_ ( (/) -cn-> CC )
72 2 a1i 
 |-  ( ( ph /\ B < A ) -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
73 simpr 
 |-  ( ( ph /\ B < A ) -> B < A )
74 24 adantr 
 |-  ( ( ph /\ B < A ) -> A e. RR* )
75 4 rexrd 
 |-  ( ph -> B e. RR* )
76 75 adantr 
 |-  ( ( ph /\ B < A ) -> B e. RR* )
77 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
78 74 76 77 syl2anc 
 |-  ( ( ph /\ B < A ) -> ( ( A [,] B ) = (/) <-> B < A ) )
79 73 78 mpbird 
 |-  ( ( ph /\ B < A ) -> ( A [,] B ) = (/) )
80 79 mpteq1d 
 |-  ( ( ph /\ B < A ) -> ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) = ( x e. (/) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
81 mpt0 
 |-  ( x e. (/) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) = (/)
82 81 a1i 
 |-  ( ( ph /\ B < A ) -> ( x e. (/) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) = (/) )
83 72 80 82 3eqtrd 
 |-  ( ( ph /\ B < A ) -> G = (/) )
84 0cnf 
 |-  (/) e. ( { (/) } Cn { (/) } )
85 83 84 eqeltrdi 
 |-  ( ( ph /\ B < A ) -> G e. ( { (/) } Cn { (/) } ) )
86 71 85 sseldi 
 |-  ( ( ph /\ B < A ) -> G e. ( (/) -cn-> CC ) )
87 79 eqcomd 
 |-  ( ( ph /\ B < A ) -> (/) = ( A [,] B ) )
88 87 oveq1d 
 |-  ( ( ph /\ B < A ) -> ( (/) -cn-> CC ) = ( ( A [,] B ) -cn-> CC ) )
89 86 88 eleqtrd 
 |-  ( ( ph /\ B < A ) -> G e. ( ( A [,] B ) -cn-> CC ) )
90 48 60 89 syl2anc 
 |-  ( ( ( ph /\ -. A < B ) /\ -. A = B ) -> G e. ( ( A [,] B ) -cn-> CC ) )
91 47 90 pm2.61dan 
 |-  ( ( ph /\ -. A < B ) -> G e. ( ( A [,] B ) -cn-> CC ) )
92 15 91 pm2.61dan 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )