Metamath Proof Explorer

Definition df-cnfld

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ` |``s restriction operator, for instance ( CCfld |`AA ) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex , cnfldadd , cnfldmul , cnfldcj , cnfldtset , cnfldle , cnfldds , and cnfldbas . We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Thierry Arnoux, 15-Dec-2017) (New usage is discouraged.)

Ref Expression
Assertion 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. - ) ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnfld 
 |-  CCfld
1 cbs 
 |-  Base
2 cnx 
 |-  ndx
3 2 1 cfv 
 |-  ( Base ` ndx )
4 cc 
 |-  CC
5 3 4 cop 
 |-  <. ( Base ` ndx ) , CC >.
6 cplusg 
 |-  +g
7 2 6 cfv 
 |-  ( +g ` ndx )
8 caddc 
 |-  +
9 7 8 cop 
 |-  <. ( +g ` ndx ) , + >.
10 cmulr 
 |-  .r
11 2 10 cfv 
 |-  ( .r ` ndx )
12 cmul 
 |-  x.
13 11 12 cop 
 |-  <. ( .r ` ndx ) , x. >.
14 5 9 13 ctp 
 |-  { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
15 cstv 
 |-  *r
16 2 15 cfv 
 |-  ( *r ` ndx )
17 ccj 
 |-  *
18 16 17 cop 
 |-  <. ( *r ` ndx ) , * >.
19 18 csn 
 |-  { <. ( *r ` ndx ) , * >. }
20 14 19 cun 
 |-  ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
21 cts 
 |-  TopSet
22 2 21 cfv 
 |-  ( TopSet ` ndx )
23 cmopn 
 |-  MetOpen
24 cabs 
 |-  abs
25 cmin 
 |-  -
26 24 25 ccom 
 |-  ( abs o. - )
27 26 23 cfv 
 |-  ( MetOpen ` ( abs o. - ) )
28 22 27 cop 
 |-  <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
29 cple 
 |-  le
30 2 29 cfv 
 |-  ( le ` ndx )
31 cle 
 |-  <_
32 30 31 cop 
 |-  <. ( le ` ndx ) , <_ >.
33 cds 
 |-  dist
34 2 33 cfv 
 |-  ( dist ` ndx )
35 34 26 cop 
 |-  <. ( dist ` ndx ) , ( abs o. - ) >.
36 28 32 35 ctp 
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
37 cunif 
 |-  UnifSet
38 2 37 cfv 
 |-  ( UnifSet ` ndx )
39 cmetu 
 |-  metUnif
40 26 39 cfv 
 |-  ( metUnif ` ( abs o. - ) )
41 38 40 cop 
 |-  <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >.
42 41 csn 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. }
43 36 42 cun 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
44 20 43 cun 
 |-  ( ( { <. ( 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. - ) ) >. } ) )
45 0 44 wceq 
 |-  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. - ) ) >. } ) )