This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncms

Description: The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cncms 
|- CCfld e. CMetSp

Proof

Step Hyp Ref Expression
1 cnfldms 
 |-  CCfld e. MetSp
2 eqid 
 |-  ( abs o. - ) = ( abs o. - )
3 2 cncmet 
 |-  ( abs o. - ) e. ( CMet ` CC )
4 cnfldbas 
 |-  CC = ( Base ` CCfld )
5 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
6 metf 
 |-  ( ( abs o. - ) e. ( Met ` CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
7 5 6 ax-mp 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
8 ffn 
 |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )
9 fnresdm 
 |-  ( ( abs o. - ) Fn ( CC X. CC ) -> ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - ) )
10 7 8 9 mp2b 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - )
11 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
12 11 reseq1i 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
13 10 12 eqtr3i 
 |-  ( abs o. - ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
14 4 13 iscms 
 |-  ( CCfld e. CMetSp <-> ( CCfld e. MetSp /\ ( abs o. - ) e. ( CMet ` CC ) ) )
15 1 3 14 mpbir2an 
 |-  CCfld e. CMetSp