Metamath Proof Explorer

Theorem cnfldfun

Description: The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT by using cnfldstr and structn0fun : in addition, it must be shown that (/) e/ CCfld . (Contributed by AV, 18-Nov-2021) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion cnfldfun ⊢ Fun ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 cnfldstr ⊢ ℂ fld Struct 1 13
2 structn0fun ⊢ ℂ fld Struct 1 13 → Fun ⁡ ℂ fld ∖ ∅
3 fvex ⊢ Base ndx ∈ V
4 cnex ⊢ ℂ ∈ V
5 3 4 opnzi ⊢ Base ndx ℂ ≠ ∅
6 5 nesymi ⊢ ¬ ∅ = Base ndx ℂ
7 fvex ⊢ + ndx ∈ V
8 mpoaddex ⊢ u ∈ ℂ , v ∈ ℂ ⟼ u + v ∈ V
9 7 8 opnzi ⊢ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ≠ ∅
10 9 nesymi ⊢ ¬ ∅ = + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v
11 fvex ⊢ ⋅ ndx ∈ V
12 mpomulex ⊢ u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ V
13 11 12 opnzi ⊢ ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ≠ ∅
14 13 nesymi ⊢ ¬ ∅ = ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v
15 3ioran ⊢ ¬ ∅ = Base ndx ℂ ∨ ∅ = + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ∨ ∅ = ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ↔ ¬ ∅ = Base ndx ℂ ∧ ¬ ∅ = + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ∧ ¬ ∅ = ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v
16 0ex ⊢ ∅ ∈ V
17 16 eltp ⊢ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ↔ ∅ = Base ndx ℂ ∨ ∅ = + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ∨ ∅ = ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v
18 15 17 xchnxbir ⊢ ¬ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ↔ ¬ ∅ = Base ndx ℂ ∧ ¬ ∅ = + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ∧ ¬ ∅ = ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v
19 6 10 14 18 mpbir3an ⊢ ¬ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v
20 fvex ⊢ * ndx ∈ V
21 cjf ⊢ * : ℂ ⟶ ℂ
22 fex ⊢ * : ℂ ⟶ ℂ ∧ ℂ ∈ V → * ∈ V
23 21 4 22 mp2an ⊢ * ∈ V
24 20 23 opnzi ⊢ * ndx * ≠ ∅
25 24 necomi ⊢ ∅ ≠ * ndx *
26 nelsn ⊢ ∅ ≠ * ndx * → ¬ ∅ ∈ * ndx *
27 25 26 ax-mp ⊢ ¬ ∅ ∈ * ndx *
28 19 27 pm3.2i ⊢ ¬ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∧ ¬ ∅ ∈ * ndx *
29 fvex ⊢ TopSet ⁡ ndx ∈ V
30 fvex ⊢ MetOpen ⁡ abs ∘ − ∈ V
31 29 30 opnzi ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≠ ∅
32 31 nesymi ⊢ ¬ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ −
33 fvex ⊢ ≤ ndx ∈ V
34 letsr ⊢ ≤ ∈ TosetRel
35 34 elexi ⊢ ≤ ∈ V
36 33 35 opnzi ⊢ ≤ ndx ≤ ≠ ∅
37 36 nesymi ⊢ ¬ ∅ = ≤ ndx ≤
38 fvex ⊢ dist ⁡ ndx ∈ V
39 absf ⊢ abs : ℂ ⟶ ℝ
40 fex ⊢ abs : ℂ ⟶ ℝ ∧ ℂ ∈ V → abs ∈ V
41 39 4 40 mp2an ⊢ abs ∈ V
42 subf ⊢ − : ℂ × ℂ ⟶ ℂ
43 4 4 xpex ⊢ ℂ × ℂ ∈ V
44 fex ⊢ − : ℂ × ℂ ⟶ ℂ ∧ ℂ × ℂ ∈ V → − ∈ V
45 42 43 44 mp2an ⊢ − ∈ V
46 41 45 coex ⊢ abs ∘ − ∈ V
47 38 46 opnzi ⊢ dist ⁡ ndx abs ∘ − ≠ ∅
48 47 nesymi ⊢ ¬ ∅ = dist ⁡ ndx abs ∘ −
49 32 37 48 3pm3.2ni ⊢ ¬ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ∨ ∅ = ≤ ndx ≤ ∨ ∅ = dist ⁡ ndx abs ∘ −
50 16 eltp ⊢ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ↔ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ∨ ∅ = ≤ ndx ≤ ∨ ∅ = dist ⁡ ndx abs ∘ −
51 49 50 mtbir ⊢ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ −
52 fvex ⊢ UnifSet ⁡ ndx ∈ V
53 fvex ⊢ metUnif ⁡ abs ∘ − ∈ V
54 52 53 opnzi ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ≠ ∅
55 54 necomi ⊢ ∅ ≠ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
56 nelsn ⊢ ∅ ≠ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − → ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
57 55 56 ax-mp ⊢ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
58 51 57 pm3.2i ⊢ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∧ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
59 28 58 pm3.2i ⊢ ¬ ∅ ∈ 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 ∘ −
60 ioran ⊢ ¬ ∅ ∈ 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 ∘ − ↔ ¬ ∅ ∈ 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 ∘ −
61 ioran ⊢ ¬ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∨ ∅ ∈ * ndx * ↔ ¬ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∧ ¬ ∅ ∈ * ndx *
62 ioran ⊢ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∨ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ↔ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∧ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
63 61 62 anbi12i ⊢ ¬ ∅ ∈ 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 ∘ − ↔ ¬ ∅ ∈ 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 ∘ −
64 60 63 bitri ⊢ ¬ ∅ ∈ 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 ∘ − ↔ ¬ ∅ ∈ 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 ∘ −
65 59 64 mpbir ⊢ ¬ ∅ ∈ 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 ∘ −
66 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 ∘ −
67 66 eleq2i ⊢ ∅ ∈ ℂ 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 ∘ −
68 elun ⊢ ∅ ∈ 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 ∘ − ↔ ∅ ∈ 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 ∘ −
69 elun ⊢ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ↔ ∅ ∈ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∨ ∅ ∈ * ndx *
70 elun ⊢ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ↔ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∨ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
71 69 70 orbi12i ⊢ ∅ ∈ 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 ∘ − ↔ ∅ ∈ 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 ∘ −
72 67 68 71 3bitri ⊢ ∅ ∈ ℂ 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 ∘ −
73 65 72 mtbir ⊢ ¬ ∅ ∈ ℂ fld
74 disjsn ⊢ ℂ fld ∩ ∅ = ∅ ↔ ¬ ∅ ∈ ℂ fld
75 73 74 mpbir ⊢ ℂ fld ∩ ∅ = ∅
76 disjdif2 ⊢ ℂ fld ∩ ∅ = ∅ → ℂ fld ∖ ∅ = ℂ fld
77 75 76 ax-mp ⊢ ℂ fld ∖ ∅ = ℂ fld
78 77 funeqi ⊢ Fun ⁡ ℂ fld ∖ ∅ ↔ Fun ⁡ ℂ fld
79 2 78 sylib ⊢ ℂ fld Struct 1 13 → Fun ⁡ ℂ fld
80 1 79 ax-mp ⊢ Fun ⁡ ℂ fld