Metamath Proof Explorer

Theorem cnfldeuf

Description: The Euclidean function component of the complex numbers. (Contributed by Thierry Arnoux, 9-Nov-2026)

Ref Expression
Assertion cnfldeuf ⊢ abs = EuclF ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 absex ⊢ abs ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 21
3 eufid ⊢ EuclF = Slot EuclF ⁡ ndx
4 snsspr2 ⊢ EuclF ⁡ ndx 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 ⊢ EuclF ⁡ ndx abs ⊆ ℂ fld
11 2 3 10 strfv ⊢ abs ∈ V → abs = EuclF ⁡ ℂ fld
12 1 11 ax-mp ⊢ abs = EuclF ⁡ ℂ fld