Metamath Proof Explorer

Theorem cncfco

Description: The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses cncfco.4 
|- ( ph -> F e. ( A -cn-> B ) )
cncfco.5 
|- ( ph -> G e. ( B -cn-> C ) )
Assertion cncfco 
|- ( ph -> ( G o. F ) e. ( A -cn-> C ) )

Proof

Step Hyp Ref Expression
1 cncfco.4 
 |-  ( ph -> F e. ( A -cn-> B ) )
2 cncfco.5 
 |-  ( ph -> G e. ( B -cn-> C ) )
3 cncff 
 |-  ( G e. ( B -cn-> C ) -> G : B --> C )
4 2 3 syl 
 |-  ( ph -> G : B --> C )
5 cncff 
 |-  ( F e. ( A -cn-> B ) -> F : A --> B )
6 1 5 syl 
 |-  ( ph -> F : A --> B )
7 fco 
 |-  ( ( G : B --> C /\ F : A --> B ) -> ( G o. F ) : A --> C )
8 4 6 7 syl2anc 
 |-  ( ph -> ( G o. F ) : A --> C )
9 2 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> G e. ( B -cn-> C ) )
10 6 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> F : A --> B )
11 simprl 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> x e. A )
12 10 11 ffvelrnd 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> ( F ` x ) e. B )
13 simprr 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> y e. RR+ )
14 cncfi 
 |-  ( ( G e. ( B -cn-> C ) /\ ( F ` x ) e. B /\ y e. RR+ ) -> E. u e. RR+ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) )
15 9 12 13 14 syl3anc 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> E. u e. RR+ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) )
16 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> F e. ( A -cn-> B ) )
17 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> x e. A )
18 simpr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> u e. RR+ )
19 cncfi 
 |-  ( ( F e. ( A -cn-> B ) /\ x e. A /\ u e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) )
21 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> F : A --> B )
22 simprr 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> w e. A )
23 21 22 ffvelrnd 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( F ` w ) e. B )
24 fvoveq1 
 |-  ( v = ( F ` w ) -> ( abs ` ( v - ( F ` x ) ) ) = ( abs ` ( ( F ` w ) - ( F ` x ) ) ) )
25 24 breq1d 
 |-  ( v = ( F ` w ) -> ( ( abs ` ( v - ( F ` x ) ) ) < u <-> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) )
26 25 imbrov2fvoveq 
 |-  ( v = ( F ` w ) -> ( ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) <-> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) )
27 26 rspcv 
 |-  ( ( F ` w ) e. B -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) )
28 23 27 syl 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) )
29 fvco3 
 |-  ( ( F : A --> B /\ w e. A ) -> ( ( G o. F ) ` w ) = ( G ` ( F ` w ) ) )
30 21 22 29 syl2anc 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( G o. F ) ` w ) = ( G ` ( F ` w ) ) )
31 17 adantr 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> x e. A )
32 fvco3 
 |-  ( ( F : A --> B /\ x e. A ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
33 21 31 32 syl2anc 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
34 30 33 oveq12d 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) = ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) )
35 34 fveq2d 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) = ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) )
36 35 breq1d 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y <-> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) )
37 36 imbi2d 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) <-> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) )
38 28 37 sylibrd 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
39 38 imp 
 |-  ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) )
40 39 an32s 
 |-  ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) )
41 40 imim2d 
 |-  ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
42 41 anassrs 
 |-  ( ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ z e. RR+ ) /\ w e. A ) -> ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
43 42 ralimdva 
 |-  ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ z e. RR+ ) -> ( A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
44 43 reximdva 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) -> ( E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
45 44 ex 
 |-  ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) )
46 20 45 mpid 
 |-  ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
47 46 rexlimdva 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> ( E. u e. RR+ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) )
48 15 47 mpd 
 |-  ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) )
49 48 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) )
50 cncfrss 
 |-  ( F e. ( A -cn-> B ) -> A C_ CC )
51 1 50 syl 
 |-  ( ph -> A C_ CC )
52 cncfrss2 
 |-  ( G e. ( B -cn-> C ) -> C C_ CC )
53 2 52 syl 
 |-  ( ph -> C C_ CC )
54 elcncf2 
 |-  ( ( A C_ CC /\ C C_ CC ) -> ( ( G o. F ) e. ( A -cn-> C ) <-> ( ( G o. F ) : A --> C /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) )
55 51 53 54 syl2anc 
 |-  ( ph -> ( ( G o. F ) e. ( A -cn-> C ) <-> ( ( G o. F ) : A --> C /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) )
56 8 49 55 mpbir2and 
 |-  ( ph -> ( G o. F ) e. ( A -cn-> C ) )