Metamath Proof Explorer

Theorem cnfldunif

Description: The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion cnfldunif ⊢ metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 fvex ⊢ metUnif ⁡ abs ∘ − ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 13
3 unifid ⊢ UnifSet = Slot UnifSet ⁡ ndx
4 ssun2 ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
5 ssun2 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
6 df-cnfld ⊢ ℂ fld = Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
7 5 6 sseqtrri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ ℂ fld
8 4 7 sstri ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ ℂ fld
9 2 3 8 strfv ⊢ metUnif ⁡ abs ∘ − ∈ V → metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld
10 1 9 ax-mp ⊢ metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld