Metamath Proof Explorer

Theorem cnflduss

Description: The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Hypothesis cnflduss.1 ⊢ U = UnifSt ⁡ ℂ fld
Assertion cnflduss ⊢ U = metUnif ⁡ abs ∘ −

Proof

Step Hyp Ref Expression
1 cnflduss.1 ⊢ U = UnifSt ⁡ ℂ fld
2 0cn ⊢ 0 ∈ ℂ
3 2 ne0ii ⊢ ℂ ≠ ∅
4 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
5 xmetpsmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ → abs ∘ − ∈ PsMet ⁡ ℂ
6 4 5 ax-mp ⊢ abs ∘ − ∈ PsMet ⁡ ℂ
7 metuust ⊢ ℂ ≠ ∅ ∧ abs ∘ − ∈ PsMet ⁡ ℂ → metUnif ⁡ abs ∘ − ∈ UnifOn ⁡ ℂ
8 3 6 7 mp2an ⊢ metUnif ⁡ abs ∘ − ∈ UnifOn ⁡ ℂ
9 ustuni ⊢ metUnif ⁡ abs ∘ − ∈ UnifOn ⁡ ℂ → ⋃ metUnif ⁡ abs ∘ − = ℂ × ℂ
10 8 9 ax-mp ⊢ ⋃ metUnif ⁡ abs ∘ − = ℂ × ℂ
11 10 eqcomi ⊢ ℂ × ℂ = ⋃ metUnif ⁡ abs ∘ −
12 cnfldbas ⊢ ℂ = Base ℂ fld
13 cnfldunif ⊢ metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld
14 12 13 ussid ⊢ ℂ × ℂ = ⋃ metUnif ⁡ abs ∘ − → metUnif ⁡ abs ∘ − = UnifSt ⁡ ℂ fld
15 11 14 ax-mp ⊢ metUnif ⁡ abs ∘ − = UnifSt ⁡ ℂ fld
16 1 15 eqtr4i ⊢ U = metUnif ⁡ abs ∘ −