Metamath Proof Explorer

Theorem cnflddsOLD

Description: Obsolete version of cnfldds as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnflddsOLD ⊢ abs ∘ − = dist ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 absf ⊢ abs : ℂ ⟶ ℝ
2 subf ⊢ − : ℂ × ℂ ⟶ ℂ
3 fco ⊢ abs : ℂ ⟶ ℝ ∧ − : ℂ × ℂ ⟶ ℂ → abs ∘ − : ℂ × ℂ ⟶ ℝ
4 1 2 3 mp2an ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ
5 cnex ⊢ ℂ ∈ V
6 5 5 xpex ⊢ ℂ × ℂ ∈ V
7 reex ⊢ ℝ ∈ V
8 fex2 ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ ∧ ℂ × ℂ ∈ V ∧ ℝ ∈ V → abs ∘ − ∈ V
9 4 6 7 8 mp3an ⊢ abs ∘ − ∈ V
10 cnfldstrOLD ⊢ ℂ fld Struct 1 13
11 dsid ⊢ dist = Slot dist ⁡ ndx
12 snsstp3 ⊢ dist ⁡ ndx abs ∘ − ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ −
13 ssun1 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
14 ssun2 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
15 dfcnfldOLD ⊢ ℂ fld = Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
16 14 15 sseqtrri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ ℂ fld
17 13 16 sstri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ⊆ ℂ fld
18 12 17 sstri ⊢ dist ⁡ ndx abs ∘ − ⊆ ℂ fld
19 10 11 18 strfv ⊢ abs ∘ − ∈ V → abs ∘ − = dist ⁡ ℂ fld
20 9 19 ax-mp ⊢ abs ∘ − = dist ⁡ ℂ fld