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

Metamath Proof Explorer

Theorem cnfldcusp

Description: The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldcusp ℂfld ∈ CUnifSp

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 1 ne0ii ⊢ ℂ ≠ ∅
3 cncms ⊢ ℂfld ∈ CMetSp
4 eqid ⊢ ( UnifSt ‘ ℂfld ) = ( UnifSt ‘ ℂfld )
5 4 cnflduss ⊢ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) )
6 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
7 absf ⊢ abs : ℂ ⟶ ℝ
8 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
9 fco ⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
10 7 8 9 mp2an ⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
11 ffn ⊢ ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
12 fnresdm ⊢ ( ( abs ∘ − ) Fn ( ℂ × ℂ ) → ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − ) )
13 10 11 12 mp2b ⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − )
14 cnfldds ⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
15 14 reseq1i ⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
16 13 15 eqtr3i ⊢ ( abs ∘ − ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
17 6 16 4 cmetcusp1 ⊢ ( ( ℂ ≠ ∅ ∧ ℂfld ∈ CMetSp ∧ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) ) ) → ℂfld ∈ CUnifSp )
18 2 3 5 17 mp3an ⊢ ℂfld ∈ CUnifSp