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

Proof

Step Hyp Ref Expression
1 cnmet ⊢ abs ∘ − ∈ Met ⁡ ℂ
2 eqid ⊢ MetOpen ⁡ abs ∘ − = MetOpen ⁡ abs ∘ −
3 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
4 2 mopntopon ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ → MetOpen ⁡ abs ∘ − ∈ TopOn ⁡ ℂ
5 cnfldbas ⊢ ℂ = Base ℂ fld
6 cnfldtset ⊢ MetOpen ⁡ abs ∘ − = TopSet ⁡ ℂ fld
7 5 6 topontopn ⊢ MetOpen ⁡ abs ∘ − ∈ TopOn ⁡ ℂ → MetOpen ⁡ abs ∘ − = TopOpen ⁡ ℂ fld
8 3 4 7 mp2b ⊢ MetOpen ⁡ abs ∘ − = TopOpen ⁡ ℂ fld
9 absf ⊢ abs : ℂ ⟶ ℝ
10 subf ⊢ − : ℂ × ℂ ⟶ ℂ
11 fco ⊢ abs : ℂ ⟶ ℝ ∧ − : ℂ × ℂ ⟶ ℂ → abs ∘ − : ℂ × ℂ ⟶ ℝ
12 9 10 11 mp2an ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ
13 ffn ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ → abs ∘ − Fn ℂ × ℂ
14 fnresdm ⊢ abs ∘ − Fn ℂ × ℂ → abs ∘ − ↾ ℂ × ℂ = abs ∘ −
15 12 13 14 mp2b ⊢ abs ∘ − ↾ ℂ × ℂ = abs ∘ −
16 cnfldds ⊢ abs ∘ − = dist ⁡ ℂ fld
17 16 reseq1i ⊢ abs ∘ − ↾ ℂ × ℂ = dist ⁡ ℂ fld ↾ ℂ × ℂ
18 15 17 eqtr3i ⊢ abs ∘ − = dist ⁡ ℂ fld ↾ ℂ × ℂ
19 8 5 18 isms2 ⊢ ℂ fld ∈ MetSp ↔ abs ∘ − ∈ Met ⁡ ℂ ∧ MetOpen ⁡ abs ∘ − = MetOpen ⁡ abs ∘ −
20 1 2 19 mpbir2an ⊢ ℂ fld ∈ MetSp