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) Revise df-cnfld . (Revised by Thierry Arnoux, 9-Nov-2026)

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

Proof

Step Hyp Ref Expression
1 fvex ⊢ metUnif ⁡ abs ∘ − ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 21
3 unifid ⊢ UnifSet = Slot UnifSet ⁡ ndx
4 snsspr1 ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs
5 ssun2 ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs
6 ssun2 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx 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 ∘ − EuclF ⁡ ndx abs
7 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 ∘ − EuclF ⁡ ndx abs
8 6 7 sseqtrri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs ⊆ ℂ fld
9 5 8 sstri ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs ⊆ ℂ fld
10 4 9 sstri ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ ℂ fld
11 2 3 10 strfv ⊢ metUnif ⁡ abs ∘ − ∈ V → metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld
12 1 11 ax-mp ⊢ metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld