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)

Ref Expression
Assertion cnfldfun ⊢Fun⁡ℂfld

Proof

Step Hyp Ref Expression
1 cnfldstr ⊢ℂfldStruct113
2 structn0fun ⊢ℂfldStruct113→Fun⁡ℂfld∖∅
3 fvex ⊢Basendx∈V
4 cnex ⊢ℂ∈V
5 3 4 opnzi ⊢Basendxℂ≠∅
6 5 nesymi ⊢¬∅=Basendxℂ
7 fvex ⊢+ndx∈V
8 addex ⊢+∈V
9 7 8 opnzi ⊢+ndx+≠∅
10 9 nesymi ⊢¬∅=+ndx+
11 fvex ⊢⋅ndx∈V
12 mulex ⊢×∈V
13 11 12 opnzi ⊢⋅ndx×≠∅
14 13 nesymi ⊢¬∅=⋅ndx×
15 3ioran ⊢¬∅=Basendxℂ∨∅=+ndx+∨∅=⋅ndx×↔¬∅=Basendxℂ∧¬∅=+ndx+∧¬∅=⋅ndx×
16 0ex ⊢∅∈V
17 16 eltp ⊢∅∈Basendxℂ+ndx+⋅ndx×↔∅=Basendxℂ∨∅=+ndx+∨∅=⋅ndx×
18 15 17 xchnxbir ⊢¬∅∈Basendxℂ+ndx+⋅ndx×↔¬∅=Basendxℂ∧¬∅=+ndx+∧¬∅=⋅ndx×
19 6 10 14 18 mpbir3an ⊢¬∅∈Basendxℂ+ndx+⋅ndx×
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 ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∧¬∅∈*ndx*
29 fvex ⊢TopSet⁡ndx∈V
30 fvex ⊢MetOpen⁡abs∘−∈V
31 29 30 opnzi ⊢TopSet⁡ndxMetOpen⁡abs∘−≠∅
32 31 nesymi ⊢¬∅=TopSet⁡ndxMetOpen⁡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⁡ndxabs∘−≠∅
48 47 nesymi ⊢¬∅=dist⁡ndxabs∘−
49 3ioran ⊢¬∅=TopSet⁡ndxMetOpen⁡abs∘−∨∅=≤ndx≤∨∅=dist⁡ndxabs∘−↔¬∅=TopSet⁡ndxMetOpen⁡abs∘−∧¬∅=≤ndx≤∧¬∅=dist⁡ndxabs∘−
50 32 37 48 49 mpbir3an ⊢¬∅=TopSet⁡ndxMetOpen⁡abs∘−∨∅=≤ndx≤∨∅=dist⁡ndxabs∘−
51 16 eltp ⊢∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−↔∅=TopSet⁡ndxMetOpen⁡abs∘−∨∅=≤ndx≤∨∅=dist⁡ndxabs∘−
52 50 51 mtbir ⊢¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−
53 fvex ⊢UnifSet⁡ndx∈V
54 fvex ⊢metUnif⁡abs∘−∈V
55 53 54 opnzi ⊢UnifSet⁡ndxmetUnif⁡abs∘−≠∅
56 55 necomi ⊢∅≠UnifSet⁡ndxmetUnif⁡abs∘−
57 nelsn ⊢∅≠UnifSet⁡ndxmetUnif⁡abs∘−→¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
58 56 57 ax-mp ⊢¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
59 52 58 pm3.2i ⊢¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∧¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
60 28 59 pm3.2i ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∧¬∅∈*ndx*∧¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∧¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
61 ioran ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−↔¬∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∧¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−
62 ioran ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*↔¬∅∈Basendxℂ+ndx+⋅ndx×∧¬∅∈*ndx*
63 ioran ⊢¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−↔¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∧¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
64 62 63 anbi12i ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∧¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−↔¬∅∈Basendxℂ+ndx+⋅ndx×∧¬∅∈*ndx*∧¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∧¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
65 61 64 bitri ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−↔¬∅∈Basendxℂ+ndx+⋅ndx×∧¬∅∈*ndx*∧¬∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∧¬∅∈UnifSet⁡ndxmetUnif⁡abs∘−
66 60 65 mpbir ⊢¬∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−
67 df-cnfld ⊢ℂfld=Basendxℂ+ndx+⋅ndx×∪*ndx*∪TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∪UnifSet⁡ndxmetUnif⁡abs∘−
68 67 eleq2i ⊢∅∈ℂfld↔∅∈Basendxℂ+ndx+⋅ndx×∪*ndx*∪TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∪UnifSet⁡ndxmetUnif⁡abs∘−
69 elun ⊢∅∈Basendxℂ+ndx+⋅ndx×∪*ndx*∪TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∪UnifSet⁡ndxmetUnif⁡abs∘−↔∅∈Basendxℂ+ndx+⋅ndx×∪*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∪UnifSet⁡ndxmetUnif⁡abs∘−
70 elun ⊢∅∈Basendxℂ+ndx+⋅ndx×∪*ndx*↔∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*
71 elun ⊢∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∪UnifSet⁡ndxmetUnif⁡abs∘−↔∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−
72 70 71 orbi12i ⊢∅∈Basendxℂ+ndx+⋅ndx×∪*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∪UnifSet⁡ndxmetUnif⁡abs∘−↔∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−
73 68 69 72 3bitri ⊢∅∈ℂfld↔∅∈Basendxℂ+ndx+⋅ndx×∨∅∈*ndx*∨∅∈TopSet⁡ndxMetOpen⁡abs∘−≤ndx≤dist⁡ndxabs∘−∨∅∈UnifSet⁡ndxmetUnif⁡abs∘−
74 66 73 mtbir ⊢¬∅∈ℂfld
75 disjsn ⊢ℂfld∩∅=∅↔¬∅∈ℂfld
76 74 75 mpbir ⊢ℂfld∩∅=∅
77 disjdif2 ⊢ℂfld∩∅=∅→ℂfld∖∅=ℂfld
78 76 77 ax-mp ⊢ℂfld∖∅=ℂfld
79 78 funeqi ⊢Fun⁡ℂfld∖∅↔Fun⁡ℂfld
80 2 79 sylib ⊢ℂfldStruct113→Fun⁡ℂfld
81 1 80 ax-mp ⊢Fun⁡ℂfld