This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 CCfld

Proof

Step Hyp Ref Expression
1 cnfldstr 
 |-  CCfld Struct <. 1 , ; 1 3 >.
2 structn0fun 
 |-  ( CCfld Struct <. 1 , ; 1 3 >. -> Fun ( CCfld \ { (/) } ) )
3 fvex 
 |-  ( Base ` ndx ) e. _V
4 cnex 
 |-  CC e. _V
5 3 4 opnzi 
 |-  <. ( Base ` ndx ) , CC >. =/= (/)
6 5 nesymi 
 |-  -. (/) = <. ( Base ` ndx ) , CC >.
7 fvex 
 |-  ( +g ` ndx ) e. _V
8 mpoaddex 
 |-  ( u e. CC , v e. CC |-> ( u + v ) ) e. _V
9 7 8 opnzi 
 |-  <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. =/= (/)
10 9 nesymi 
 |-  -. (/) = <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >.
11 fvex 
 |-  ( .r ` ndx ) e. _V
12 mpomulex 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. _V
13 11 12 opnzi 
 |-  <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. =/= (/)
14 13 nesymi 
 |-  -. (/) = <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >.
15 3ioran 
 |-  ( -. ( (/) = <. ( Base ` ndx ) , CC >. \/ (/) = <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. \/ (/) = <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. ) <-> ( -. (/) = <. ( Base ` ndx ) , CC >. /\ -. (/) = <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. /\ -. (/) = <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. ) )
16 0ex 
 |-  (/) e. _V
17 16 eltp 
 |-  ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } <-> ( (/) = <. ( Base ` ndx ) , CC >. \/ (/) = <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. \/ (/) = <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. ) )
18 15 17 xchnxbir 
 |-  ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } <-> ( -. (/) = <. ( Base ` ndx ) , CC >. /\ -. (/) = <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. /\ -. (/) = <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. ) )
19 6 10 14 18 mpbir3an 
 |-  -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. }
20 fvex 
 |-  ( *r ` ndx ) e. _V
21 cjf 
 |-  * : CC --> CC
22 fex 
 |-  ( ( * : CC --> CC /\ CC e. _V ) -> * e. _V )
23 21 4 22 mp2an 
 |-  * e. _V
24 20 23 opnzi 
 |-  <. ( *r ` ndx ) , * >. =/= (/)
25 24 necomi 
 |-  (/) =/= <. ( *r ` ndx ) , * >.
26 nelsn 
 |-  ( (/) =/= <. ( *r ` ndx ) , * >. -> -. (/) e. { <. ( *r ` ndx ) , * >. } )
27 25 26 ax-mp 
 |-  -. (/) e. { <. ( *r ` ndx ) , * >. }
28 19 27 pm3.2i 
 |-  ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } )
29 fvex 
 |-  ( TopSet ` ndx ) e. _V
30 fvex 
 |-  ( MetOpen ` ( abs o. - ) ) e. _V
31 29 30 opnzi 
 |-  <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. =/= (/)
32 31 nesymi 
 |-  -. (/) = <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
33 fvex 
 |-  ( le ` ndx ) e. _V
34 letsr 
 |-  <_ e. TosetRel
35 34 elexi 
 |-  <_ e. _V
36 33 35 opnzi 
 |-  <. ( le ` ndx ) , <_ >. =/= (/)
37 36 nesymi 
 |-  -. (/) = <. ( le ` ndx ) , <_ >.
38 fvex 
 |-  ( dist ` ndx ) e. _V
39 absf 
 |-  abs : CC --> RR
40 fex 
 |-  ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V )
41 39 4 40 mp2an 
 |-  abs e. _V
42 subf 
 |-  - : ( CC X. CC ) --> CC
43 4 4 xpex 
 |-  ( CC X. CC ) e. _V
44 fex 
 |-  ( ( - : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V ) -> - e. _V )
45 42 43 44 mp2an 
 |-  - e. _V
46 41 45 coex 
 |-  ( abs o. - ) e. _V
47 38 46 opnzi 
 |-  <. ( dist ` ndx ) , ( abs o. - ) >. =/= (/)
48 47 nesymi 
 |-  -. (/) = <. ( dist ` ndx ) , ( abs o. - ) >.
49 32 37 48 3pm3.2ni 
 |-  -. ( (/) = <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. \/ (/) = <. ( le ` ndx ) , <_ >. \/ (/) = <. ( dist ` ndx ) , ( abs o. - ) >. )
50 16 eltp 
 |-  ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } <-> ( (/) = <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. \/ (/) = <. ( le ` ndx ) , <_ >. \/ (/) = <. ( dist ` ndx ) , ( abs o. - ) >. ) )
51 49 50 mtbir 
 |-  -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
52 fvex 
 |-  ( UnifSet ` ndx ) e. _V
53 fvex 
 |-  ( metUnif ` ( abs o. - ) ) e. _V
54 52 53 opnzi 
 |-  <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. =/= (/)
55 54 necomi 
 |-  (/) =/= <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >.
56 nelsn 
 |-  ( (/) =/= <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. -> -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
57 55 56 ax-mp 
 |-  -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. }
58 51 57 pm3.2i 
 |-  ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
59 28 58 pm3.2i 
 |-  ( ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) /\ ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
60 ioran 
 |-  ( -. ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( -. ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) /\ -. ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
61 ioran 
 |-  ( -. ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) <-> ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) )
62 ioran 
 |-  ( -. ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) <-> ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
63 61 62 anbi12i 
 |-  ( ( -. ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) /\ -. ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) /\ ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
64 60 63 bitri 
 |-  ( -. ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) /\ ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
65 59 64 mpbir 
 |-  -. ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
66 df-cnfld 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
67 66 eleq2i 
 |-  ( (/) e. CCfld <-> (/) e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
68 elun 
 |-  ( (/) e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( (/) e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) \/ (/) e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
69 elun 
 |-  ( (/) e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) <-> ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) )
70 elun 
 |-  ( (/) e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) <-> ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
71 69 70 orbi12i 
 |-  ( ( (/) e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) \/ (/) e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
72 67 68 71 3bitri 
 |-  ( (/) e. CCfld <-> ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
73 65 72 mtbir 
 |-  -. (/) e. CCfld
74 disjsn 
 |-  ( ( CCfld i^i { (/) } ) = (/) <-> -. (/) e. CCfld )
75 73 74 mpbir 
 |-  ( CCfld i^i { (/) } ) = (/)
76 disjdif2 
 |-  ( ( CCfld i^i { (/) } ) = (/) -> ( CCfld \ { (/) } ) = CCfld )
77 75 76 ax-mp 
 |-  ( CCfld \ { (/) } ) = CCfld
78 77 funeqi 
 |-  ( Fun ( CCfld \ { (/) } ) <-> Fun CCfld )
79 2 78 sylib 
 |-  ( CCfld Struct <. 1 , ; 1 3 >. -> Fun CCfld )
80 1 79 ax-mp 
 |-  Fun CCfld