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

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