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

Definition df-cnfld 16706
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 16708, cnfldadd 16710, cnfldmul 16711, cnfldcj 16712, cnfldtset 16713, cnfldle 16714, cnfldds 16715, and cnfldbas 16709. 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.)

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.  -  ) >. }  u.  { <. ( UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. } ) )

Detailed syntax breakdown of Definition df-cnfld
StepHypRef Expression
1 ccnfld 16705 . 2  classfld
2 cnx 13468 . . . . . . 7  class  ndx
3 cbs 13471 . . . . . . 7  class  Base
42, 3cfv 5456 . . . . . 6  class  ( Base `  ndx )
5 cc 8990 . . . . . 6  class  CC
64, 5cop 3819 . . . . 5  class  <. ( Base `  ndx ) ,  CC >.
7 cplusg 13531 . . . . . . 7  class  +g
82, 7cfv 5456 . . . . . 6  class  ( +g  ` 
ndx )
9 caddc 8995 . . . . . 6  class  +
108, 9cop 3819 . . . . 5  class  <. ( +g  `  ndx ) ,  +  >.
11 cmulr 13532 . . . . . . 7  class  .r
122, 11cfv 5456 . . . . . 6  class  ( .r
`  ndx )
13 cmul 8997 . . . . . 6  class  x.
1412, 13cop 3819 . . . . 5  class  <. ( .r `  ndx ) ,  x.  >.
156, 10, 14ctp 3818 . . . 4  class  { <. (
Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }
16 cstv 13533 . . . . . . 7  class  * r
172, 16cfv 5456 . . . . . 6  class  ( * r `  ndx )
18 ccj 11903 . . . . . 6  class  *
1917, 18cop 3819 . . . . 5  class  <. (
* r `  ndx ) ,  * >.
2019csn 3816 . . . 4  class  { <. ( * r `  ndx ) ,  * >. }
2115, 20cun 3320 . . 3  class  ( {
<. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )
22 cts 13537 . . . . . . 7  class TopSet
232, 22cfv 5456 . . . . . 6  class  (TopSet `  ndx )
24 cabs 12041 . . . . . . . 8  class  abs
25 cmin 9293 . . . . . . . 8  class  -
2624, 25ccom 4884 . . . . . . 7  class  ( abs 
o.  -  )
27 cmopn 16693 . . . . . . 7  class  MetOpen
2826, 27cfv 5456 . . . . . 6  class  ( MetOpen `  ( abs  o.  -  )
)
2923, 28cop 3819 . . . . 5  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >.
30 cple 13538 . . . . . . 7  class  le
312, 30cfv 5456 . . . . . 6  class  ( le
`  ndx )
32 cle 9123 . . . . . 6  class  <_
3331, 32cop 3819 . . . . 5  class  <. ( le `  ndx ) ,  <_  >.
34 cds 13540 . . . . . . 7  class  dist
352, 34cfv 5456 . . . . . 6  class  ( dist `  ndx )
3635, 26cop 3819 . . . . 5  class  <. ( dist `  ndx ) ,  ( abs  o.  -  ) >.
3729, 33, 36ctp 3818 . . . 4  class  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }
38 cunif 13541 . . . . . . 7  class  UnifSet
392, 38cfv 5456 . . . . . 6  class  ( UnifSet ` 
ndx )
40 cmetu 16695 . . . . . . 7  class metUnif
4126, 40cfv 5456 . . . . . 6  class  (metUnif `  ( abs  o.  -  ) )
4239, 41cop 3819 . . . . 5  class  <. ( UnifSet
`  ndx ) ,  (metUnif `  ( abs  o.  -  ) ) >.
4342csn 3816 . . . 4  class  { <. (
UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. }
4437, 43cun 3320 . . 3  class  ( {
<. (TopSet `  ndx ) ,  ( MetOpen `  ( abs  o. 
-  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }  u.  { <. ( UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. } )
4521, 44cun 3320 . 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.  -  ) >. }  u.  { <. ( UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. } ) )
461, 45wceq 1653 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.  -  ) >. }  u.  { <. ( UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. } ) )
Colors of variables: wff set class
This definition is referenced by:  cnfldstr  16707  cnfldbas  16709  cnfldadd  16710  cnfldmul  16711  cnfldcj  16712  cnfldtset  16713  cnfldle  16714  cnfldds  16715  cnfldunif  16716
  Copyright terms: Public domain W3C validator