Metamath Proof Explorer

Theorem cncfmet

Description: Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Hypotheses cncfmet.1 
|- C = ( ( abs o. - ) |` ( A X. A ) )
cncfmet.2 
|- D = ( ( abs o. - ) |` ( B X. B ) )
cncfmet.3 
|- J = ( MetOpen ` C )
cncfmet.4 
|- K = ( MetOpen ` D )
Assertion cncfmet 
|- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 cncfmet.1 
 |-  C = ( ( abs o. - ) |` ( A X. A ) )
2 cncfmet.2 
 |-  D = ( ( abs o. - ) |` ( B X. B ) )
3 cncfmet.3 
 |-  J = ( MetOpen ` C )
4 cncfmet.4 
 |-  K = ( MetOpen ` D )
5 simplll 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> A C_ CC )
6 simprl 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> x e. A )
7 simprr 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> w e. A )
8 1 oveqi 
 |-  ( x C w ) = ( x ( ( abs o. - ) |` ( A X. A ) ) w )
9 ovres 
 |-  ( ( x e. A /\ w e. A ) -> ( x ( ( abs o. - ) |` ( A X. A ) ) w ) = ( x ( abs o. - ) w ) )
10 8 9 syl5eq 
 |-  ( ( x e. A /\ w e. A ) -> ( x C w ) = ( x ( abs o. - ) w ) )
11 10 ad2ant2l 
 |-  ( ( ( A C_ CC /\ x e. A ) /\ ( A C_ CC /\ w e. A ) ) -> ( x C w ) = ( x ( abs o. - ) w ) )
12 ssel2 
 |-  ( ( A C_ CC /\ x e. A ) -> x e. CC )
13 ssel2 
 |-  ( ( A C_ CC /\ w e. A ) -> w e. CC )
14 eqid 
 |-  ( abs o. - ) = ( abs o. - )
15 14 cnmetdval 
 |-  ( ( x e. CC /\ w e. CC ) -> ( x ( abs o. - ) w ) = ( abs ` ( x - w ) ) )
16 12 13 15 syl2an 
 |-  ( ( ( A C_ CC /\ x e. A ) /\ ( A C_ CC /\ w e. A ) ) -> ( x ( abs o. - ) w ) = ( abs ` ( x - w ) ) )
17 11 16 eqtrd 
 |-  ( ( ( A C_ CC /\ x e. A ) /\ ( A C_ CC /\ w e. A ) ) -> ( x C w ) = ( abs ` ( x - w ) ) )
18 5 6 5 7 17 syl22anc 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( x C w ) = ( abs ` ( x - w ) ) )
19 18 breq1d 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( x C w ) < z <-> ( abs ` ( x - w ) ) < z ) )
20 ffvelrn 
 |-  ( ( f : A --> B /\ x e. A ) -> ( f ` x ) e. B )
21 20 ad2ant2lr 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` x ) e. B )
22 ffvelrn 
 |-  ( ( f : A --> B /\ w e. A ) -> ( f ` w ) e. B )
23 22 ad2ant2l 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` w ) e. B )
24 2 oveqi 
 |-  ( ( f ` x ) D ( f ` w ) ) = ( ( f ` x ) ( ( abs o. - ) |` ( B X. B ) ) ( f ` w ) )
25 ovres 
 |-  ( ( ( f ` x ) e. B /\ ( f ` w ) e. B ) -> ( ( f ` x ) ( ( abs o. - ) |` ( B X. B ) ) ( f ` w ) ) = ( ( f ` x ) ( abs o. - ) ( f ` w ) ) )
26 24 25 syl5eq 
 |-  ( ( ( f ` x ) e. B /\ ( f ` w ) e. B ) -> ( ( f ` x ) D ( f ` w ) ) = ( ( f ` x ) ( abs o. - ) ( f ` w ) ) )
27 21 23 26 syl2anc 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( f ` x ) D ( f ` w ) ) = ( ( f ` x ) ( abs o. - ) ( f ` w ) ) )
28 simpllr 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> B C_ CC )
29 28 21 sseldd 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` x ) e. CC )
30 28 23 sseldd 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` w ) e. CC )
31 14 cnmetdval 
 |-  ( ( ( f ` x ) e. CC /\ ( f ` w ) e. CC ) -> ( ( f ` x ) ( abs o. - ) ( f ` w ) ) = ( abs ` ( ( f ` x ) - ( f ` w ) ) ) )
32 29 30 31 syl2anc 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( f ` x ) ( abs o. - ) ( f ` w ) ) = ( abs ` ( ( f ` x ) - ( f ` w ) ) ) )
33 27 32 eqtrd 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( f ` x ) D ( f ` w ) ) = ( abs ` ( ( f ` x ) - ( f ` w ) ) ) )
34 33 breq1d 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( ( f ` x ) D ( f ` w ) ) < y <-> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) )
35 19 34 imbi12d 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) )
36 35 anassrs 
 |-  ( ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) /\ w e. A ) -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) )
37 36 ralbidva 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) -> ( A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) )
38 37 rexbidv 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) -> ( E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) )
39 38 ralbidv 
 |-  ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) -> ( A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) )
40 39 ralbidva 
 |-  ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) -> ( A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) )
41 40 pm5.32da 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) )
42 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
43 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A C_ CC ) -> ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) )
44 42 43 mpan 
 |-  ( A C_ CC -> ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) )
45 1 44 eqeltrid 
 |-  ( A C_ CC -> C e. ( *Met ` A ) )
46 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ B C_ CC ) -> ( ( abs o. - ) |` ( B X. B ) ) e. ( *Met ` B ) )
47 42 46 mpan 
 |-  ( B C_ CC -> ( ( abs o. - ) |` ( B X. B ) ) e. ( *Met ` B ) )
48 2 47 eqeltrid 
 |-  ( B C_ CC -> D e. ( *Met ` B ) )
49 3 4 metcn 
 |-  ( ( C e. ( *Met ` A ) /\ D e. ( *Met ` B ) ) -> ( f e. ( J Cn K ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) )
50 45 48 49 syl2an 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( f e. ( J Cn K ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) )
51 elcncf 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( f e. ( A -cn-> B ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) )
52 41 50 51 3bitr4rd 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( f e. ( A -cn-> B ) <-> f e. ( J Cn K ) ) )
53 52 eqrdv 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( J Cn K ) )