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 ⊢ ℂ fld ∈ CMetSp

Proof

Step Hyp Ref Expression
1 cnfldms ⊢ ℂ fld ∈ MetSp
2 eqid ⊢ abs ∘ − = abs ∘ −
3 2 cncmet ⊢ abs ∘ − ∈ CMet ⁡ ℂ
4 cnfldbas ⊢ ℂ = Base ℂ fld
5 cnmet ⊢ abs ∘ − ∈ Met ⁡ ℂ
6 metf ⊢ abs ∘ − ∈ Met ⁡ ℂ → abs ∘ − : ℂ × ℂ ⟶ ℝ
7 5 6 ax-mp ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ
8 ffn ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ → abs ∘ − Fn ℂ × ℂ
9 fnresdm ⊢ abs ∘ − Fn ℂ × ℂ → abs ∘ − ↾ ℂ × ℂ = abs ∘ −
10 7 8 9 mp2b ⊢ abs ∘ − ↾ ℂ × ℂ = abs ∘ −
11 cnfldds ⊢ abs ∘ − = dist ⁡ ℂ fld
12 11 reseq1i ⊢ abs ∘ − ↾ ℂ × ℂ = dist ⁡ ℂ fld ↾ ℂ × ℂ
13 10 12 eqtr3i ⊢ abs ∘ − = dist ⁡ ℂ fld ↾ ℂ × ℂ
14 4 13 iscms ⊢ ℂ fld ∈ CMetSp ↔ ℂ fld ∈ MetSp ∧ abs ∘ − ∈ CMet ⁡ ℂ
15 1 3 14 mpbir2an ⊢ ℂ fld ∈ CMetSp