Metamath Proof Explorer

Theorem cncfcn

Description: Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Hypotheses cncfcn.2 
|- J = ( TopOpen ` CCfld )
cncfcn.3 
|- K = ( J |`t A )
cncfcn.4 
|- L = ( J |`t B )
Assertion cncfcn 
|- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( K Cn L ) )

Proof

Step Hyp Ref Expression
1 cncfcn.2 
 |-  J = ( TopOpen ` CCfld )
2 cncfcn.3 
 |-  K = ( J |`t A )
3 cncfcn.4 
 |-  L = ( J |`t B )
4 eqid 
 |-  ( ( abs o. - ) |` ( A X. A ) ) = ( ( abs o. - ) |` ( A X. A ) )
5 eqid 
 |-  ( ( abs o. - ) |` ( B X. B ) ) = ( ( abs o. - ) |` ( B X. B ) )
6 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )
7 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) )
8 4 5 6 7 cncfmet 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) Cn ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) ) ) )
9 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
10 simpl 
 |-  ( ( A C_ CC /\ B C_ CC ) -> A C_ CC )
11 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
12 4 11 6 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A C_ CC ) -> ( J |`t A ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
13 9 10 12 sylancr 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( J |`t A ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
14 2 13 eqtrid 
 |-  ( ( A C_ CC /\ B C_ CC ) -> K = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
15 simpr 
 |-  ( ( A C_ CC /\ B C_ CC ) -> B C_ CC )
16 5 11 7 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ B C_ CC ) -> ( J |`t B ) = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) ) )
17 9 15 16 sylancr 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( J |`t B ) = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) ) )
18 3 17 eqtrid 
 |-  ( ( A C_ CC /\ B C_ CC ) -> L = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) ) )
19 14 18 oveq12d 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( K Cn L ) = ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) Cn ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) ) ) )
20 8 19 eqtr4d 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( K Cn L ) )