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