# 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 ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$

### Proof

Step Hyp Ref Expression
1 cnmet ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$
2 eqid ${⊢}\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
3 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
4 2 mopntopon ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\to \mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{TopOn}\left(ℂ\right)$
5 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
6 cnfldtset ${⊢}\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{TopSet}\left({ℂ}_{\mathrm{fld}}\right)$
7 5 6 topontopn ${⊢}\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{TopOn}\left(ℂ\right)\to \mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
8 3 4 7 mp2b ${⊢}\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
9 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
10 subf ${⊢}-:ℂ×ℂ⟶ℂ$
11 fco ${⊢}\left(\mathrm{abs}:ℂ⟶ℝ\wedge -:ℂ×ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
12 9 10 11 mp2an ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
13 ffn ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ\to \left(\mathrm{abs}\circ -\right)Fn\left(ℂ×ℂ\right)$
14 fnresdm ${⊢}\left(\mathrm{abs}\circ -\right)Fn\left(ℂ×ℂ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left(ℂ×ℂ\right)}=\mathrm{abs}\circ -$
15 12 13 14 mp2b ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(ℂ×ℂ\right)}=\mathrm{abs}\circ -$
16 cnfldds ${⊢}\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$
17 16 reseq1i ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(ℂ×ℂ\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)↾}_{\left(ℂ×ℂ\right)}$
18 15 17 eqtr3i ${⊢}\mathrm{abs}\circ -={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)↾}_{\left(ℂ×ℂ\right)}$
19 8 5 18 isms2 ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}↔\left(\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\wedge \mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\right)$
20 1 2 19 mpbir2an ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$