Metamath Proof Explorer

Theorem cnfldfunALT

Description: Alternate proof of cnfldfun (much shorter proof, using cnfldstr and structn0fun : in addition, it must be shown that (/) e/ CCfld ). (Contributed by AV, 18-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunALT 
|- 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 addex 
 |-  + e. _V
9 7 8 opnzi 
 |-  <. ( +g ` ndx ) , + >. =/= (/)
10 9 nesymi 
 |-  -. (/) = <. ( +g ` ndx ) , + >.
11 fvex 
 |-  ( .r ` ndx ) e. _V
12 mulex 
 |-  x. e. _V
13 11 12 opnzi 
 |-  <. ( .r ` ndx ) , x. >. =/= (/)
14 13 nesymi 
 |-  -. (/) = <. ( .r ` ndx ) , x. >.
15 3ioran 
 |-  ( -. ( (/) = <. ( Base ` ndx ) , CC >. \/ (/) = <. ( +g ` ndx ) , + >. \/ (/) = <. ( .r ` ndx ) , x. >. ) <-> ( -. (/) = <. ( Base ` ndx ) , CC >. /\ -. (/) = <. ( +g ` ndx ) , + >. /\ -. (/) = <. ( .r ` ndx ) , x. >. ) )
16 0ex 
 |-  (/) e. _V
17 16 eltp 
 |-  ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } <-> ( (/) = <. ( Base ` ndx ) , CC >. \/ (/) = <. ( +g ` ndx ) , + >. \/ (/) = <. ( .r ` ndx ) , x. >. ) )
18 15 17 xchnxbir 
 |-  ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } <-> ( -. (/) = <. ( Base ` ndx ) , CC >. /\ -. (/) = <. ( +g ` ndx ) , + >. /\ -. (/) = <. ( .r ` ndx ) , x. >. ) )
19 6 10 14 18 mpbir3an 
 |-  -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
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 ) , + >. , <. ( .r ` ndx ) , x. >. } /\ -. (/) 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 3ioran 
 |-  ( -. ( (/) = <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. \/ (/) = <. ( le ` ndx ) , <_ >. \/ (/) = <. ( dist ` ndx ) , ( abs o. - ) >. ) <-> ( -. (/) = <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. /\ -. (/) = <. ( le ` ndx ) , <_ >. /\ -. (/) = <. ( dist ` ndx ) , ( abs o. - ) >. ) )
50 32 37 48 49 mpbir3an 
 |-  -. ( (/) = <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. \/ (/) = <. ( le ` ndx ) , <_ >. \/ (/) = <. ( dist ` ndx ) , ( abs o. - ) >. )
51 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. - ) >. ) )
52 50 51 mtbir 
 |-  -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
53 fvex 
 |-  ( UnifSet ` ndx ) e. _V
54 fvex 
 |-  ( metUnif ` ( abs o. - ) ) e. _V
55 53 54 opnzi 
 |-  <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. =/= (/)
56 55 necomi 
 |-  (/) =/= <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >.
57 nelsn 
 |-  ( (/) =/= <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. -> -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
58 56 57 ax-mp 
 |-  -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. }
59 52 58 pm3.2i 
 |-  ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
60 28 59 pm3.2i 
 |-  ( ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } /\ -. (/) 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 ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) 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 ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) /\ -. ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
62 ioran 
 |-  ( -. ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) <-> ( -. (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) )
63 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. - ) ) >. } ) )
64 62 63 anbi12i 
 |-  ( ( -. ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) 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 ) , + >. , <. ( .r ` ndx ) , x. >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) /\ ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
65 61 64 bitri 
 |-  ( -. ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) 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 ) , + >. , <. ( .r ` ndx ) , x. >. } /\ -. (/) e. { <. ( *r ` ndx ) , * >. } ) /\ ( -. (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ -. (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
66 60 65 mpbir 
 |-  -. ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
67 df-cnfld 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
68 67 eleq2i 
 |-  ( (/) e. CCfld <-> (/) e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( 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 ) , + >. , <. ( .r ` ndx ) , x. >. } 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 ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ (/) e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
70 elun 
 |-  ( (/) e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) <-> ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) )
71 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. - ) ) >. } ) )
72 70 71 orbi12i 
 |-  ( ( (/) e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } 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 ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
73 68 69 72 3bitri 
 |-  ( (/) e. CCfld <-> ( ( (/) e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ (/) e. { <. ( *r ` ndx ) , * >. } ) \/ ( (/) e. { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } \/ (/) e. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
74 66 73 mtbir 
 |-  -. (/) e. CCfld
75 disjsn 
 |-  ( ( CCfld i^i { (/) } ) = (/) <-> -. (/) e. CCfld )
76 74 75 mpbir 
 |-  ( CCfld i^i { (/) } ) = (/)
77 disjdif2 
 |-  ( ( CCfld i^i { (/) } ) = (/) -> ( CCfld \ { (/) } ) = CCfld )
78 76 77 ax-mp 
 |-  ( CCfld \ { (/) } ) = CCfld
79 78 funeqi 
 |-  ( Fun ( CCfld \ { (/) } ) <-> Fun CCfld )
80 2 79 sylib 
 |-  ( CCfld Struct <. 1 , ; 1 3 >. -> Fun CCfld )
81 1 80 ax-mp 
 |-  Fun CCfld