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