Metamath Proof Explorer

Theorem cnfldms

Description: The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Assertion cnfldms 
|- CCfld e. MetSp

Proof

Step Hyp Ref Expression
1 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
2 eqid 
 |-  ( MetOpen ` ( abs o. - ) ) = ( MetOpen ` ( abs o. - ) )
3 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
4 2 mopntopon 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> ( MetOpen ` ( abs o. - ) ) e. ( TopOn ` CC ) )
5 cnfldbas 
 |-  CC = ( Base ` CCfld )
6 cnfldtset 
 |-  ( MetOpen ` ( abs o. - ) ) = ( TopSet ` CCfld )
7 5 6 topontopn 
 |-  ( ( MetOpen ` ( abs o. - ) ) e. ( TopOn ` CC ) -> ( MetOpen ` ( abs o. - ) ) = ( TopOpen ` CCfld ) )
8 3 4 7 mp2b 
 |-  ( MetOpen ` ( abs o. - ) ) = ( TopOpen ` CCfld )
9 absf 
 |-  abs : CC --> RR
10 subf 
 |-  - : ( CC X. CC ) --> CC
11 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
12 9 10 11 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
13 ffn 
 |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )
14 fnresdm 
 |-  ( ( abs o. - ) Fn ( CC X. CC ) -> ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - ) )
15 12 13 14 mp2b 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - )
16 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
17 16 reseq1i 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
18 15 17 eqtr3i 
 |-  ( abs o. - ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
19 8 5 18 isms2 
 |-  ( CCfld e. MetSp <-> ( ( abs o. - ) e. ( Met ` CC ) /\ ( MetOpen ` ( abs o. - ) ) = ( MetOpen ` ( abs o. - ) ) ) )
20 1 2 19 mpbir2an 
 |-  CCfld e. MetSp