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

### Proof

Step Hyp Ref Expression
1 cnfldms ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$
2 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
3 2 cncmet ${⊢}\mathrm{abs}\circ -\in \mathrm{CMet}\left(ℂ\right)$
4 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
5 cnmet ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$
6 metf ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
7 5 6 ax-mp ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
8 ffn ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ\to \left(\mathrm{abs}\circ -\right)Fn\left(ℂ×ℂ\right)$
9 fnresdm ${⊢}\left(\mathrm{abs}\circ -\right)Fn\left(ℂ×ℂ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left(ℂ×ℂ\right)}=\mathrm{abs}\circ -$
10 7 8 9 mp2b ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(ℂ×ℂ\right)}=\mathrm{abs}\circ -$
11 cnfldds ${⊢}\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$
12 11 reseq1i ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(ℂ×ℂ\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)↾}_{\left(ℂ×ℂ\right)}$
13 10 12 eqtr3i ${⊢}\mathrm{abs}\circ -={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)↾}_{\left(ℂ×ℂ\right)}$
14 4 13 iscms ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}↔\left({ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}\wedge \mathrm{abs}\circ -\in \mathrm{CMet}\left(ℂ\right)\right)$
15 1 3 14 mpbir2an ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}$