MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnfld Unicode version

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

The contract of this set is defined entirely by cnfldex 16380, cnfldadd 16384, cnfldmul 16385, cnfldcj 16386, cnfldtset 16387, cnfldle 16388, cnfldds 16389, and cnfldbas 16383. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (New usage is discouraged.)

Assertion
Ref Expression
df-cnfld  |-fld  =  ( ( { <. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )  u.  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. } )

Detailed syntax breakdown of Definition df-cnfld
StepHypRef Expression
1 ccnfld 16377 . 2  classfld
2 cnx 13145 . . . . . . 7  class  ndx
3 cbs 13148 . . . . . . 7  class  Base
42, 3cfv 5255 . . . . . 6  class  ( Base `  ndx )
5 cc 8735 . . . . . 6  class  CC
64, 5cop 3643 . . . . 5  class  <. ( Base `  ndx ) ,  CC >.
7 cplusg 13208 . . . . . . 7  class  +g
82, 7cfv 5255 . . . . . 6  class  ( +g  ` 
ndx )
9 caddc 8740 . . . . . 6  class  +
108, 9cop 3643 . . . . 5  class  <. ( +g  `  ndx ) ,  +  >.
11 cmulr 13209 . . . . . . 7  class  .r
122, 11cfv 5255 . . . . . 6  class  ( .r
`  ndx )
13 cmul 8742 . . . . . 6  class  x.
1412, 13cop 3643 . . . . 5  class  <. ( .r `  ndx ) ,  x.  >.
156, 10, 14ctp 3642 . . . 4  class  { <. (
Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }
16 cstv 13210 . . . . . . 7  class  * r
172, 16cfv 5255 . . . . . 6  class  ( * r `  ndx )
18 ccj 11581 . . . . . 6  class  *
1917, 18cop 3643 . . . . 5  class  <. (
* r `  ndx ) ,  * >.
2019csn 3640 . . . 4  class  { <. ( * r `  ndx ) ,  * >. }
2115, 20cun 3150 . . 3  class  ( {
<. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )
22 cts 13214 . . . . . 6  class TopSet
232, 22cfv 5255 . . . . 5  class  (TopSet `  ndx )
24 cabs 11719 . . . . . . 7  class  abs
25 cmin 9037 . . . . . . 7  class  -
2624, 25ccom 4693 . . . . . 6  class  ( abs 
o.  -  )
27 cmopn 16372 . . . . . 6  class  MetOpen
2826, 27cfv 5255 . . . . 5  class  ( MetOpen `  ( abs  o.  -  )
)
2923, 28cop 3643 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >.
30 cple 13215 . . . . . 6  class  le
312, 30cfv 5255 . . . . 5  class  ( le
`  ndx )
32 cle 8868 . . . . 5  class  <_
3331, 32cop 3643 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
34 cds 13217 . . . . . 6  class  dist
352, 34cfv 5255 . . . . 5  class  ( dist `  ndx )
3635, 26cop 3643 . . . 4  class  <. ( dist `  ndx ) ,  ( abs  o.  -  ) >.
3729, 33, 36ctp 3642 . . 3  class  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }
3821, 37cun 3150 . 2  class  ( ( { <. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )  u.  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. } )
391, 38wceq 1623 1  wfffld  =  ( ( { <. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )  u.  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. } )
Colors of variables: wff set class
This definition is referenced by:  cnfldstr  16379  cnfldbas  16383  cnfldadd  16384  cnfldmul  16385  cnfldcj  16386  cnfldtset  16387  cnfldle  16388  cnfldds  16389
  Copyright terms: Public domain W3C validator