# 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