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 ) )