This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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