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