# 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`