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

Definition df-cnfld 16394
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 16396, cnfldadd 16400, cnfldmul 16401, cnfldcj 16402, cnfldtset 16403, cnfldle 16404, cnfldds 16405, and cnfldbas 16399. 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 16393 . 2  classfld
2 cnx 13161 . . . . . . 7  class  ndx
3 cbs 13164 . . . . . . 7  class  Base
42, 3cfv 5271 . . . . . 6  class  ( Base `  ndx )
5 cc 8751 . . . . . 6  class  CC
64, 5cop 3656 . . . . 5  class  <. ( Base `  ndx ) ,  CC >.
7 cplusg 13224 . . . . . . 7  class  +g
82, 7cfv 5271 . . . . . 6  class  ( +g  ` 
ndx )
9 caddc 8756 . . . . . 6  class  +
108, 9cop 3656 . . . . 5  class  <. ( +g  `  ndx ) ,  +  >.
11 cmulr 13225 . . . . . . 7  class  .r
122, 11cfv 5271 . . . . . 6  class  ( .r
`  ndx )
13 cmul 8758 . . . . . 6  class  x.
1412, 13cop 3656 . . . . 5  class  <. ( .r `  ndx ) ,  x.  >.
156, 10, 14ctp 3655 . . . 4  class  { <. (
Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }
16 cstv 13226 . . . . . . 7  class  * r
172, 16cfv 5271 . . . . . 6  class  ( * r `  ndx )
18 ccj 11597 . . . . . 6  class  *
1917, 18cop 3656 . . . . 5  class  <. (
* r `  ndx ) ,  * >.
2019csn 3653 . . . 4  class  { <. ( * r `  ndx ) ,  * >. }
2115, 20cun 3163 . . 3  class  ( {
<. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )
22 cts 13230 . . . . . 6  class TopSet
232, 22cfv 5271 . . . . 5  class  (TopSet `  ndx )
24 cabs 11735 . . . . . . 7  class  abs
25 cmin 9053 . . . . . . 7  class  -
2624, 25ccom 4709 . . . . . 6  class  ( abs 
o.  -  )
27 cmopn 16388 . . . . . 6  class  MetOpen
2826, 27cfv 5271 . . . . 5  class  ( MetOpen `  ( abs  o.  -  )
)
2923, 28cop 3656 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >.
30 cple 13231 . . . . . 6  class  le
312, 30cfv 5271 . . . . 5  class  ( le
`  ndx )
32 cle 8884 . . . . 5  class  <_
3331, 32cop 3656 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
34 cds 13233 . . . . . 6  class  dist
352, 34cfv 5271 . . . . 5  class  ( dist `  ndx )
3635, 26cop 3656 . . . 4  class  <. ( dist `  ndx ) ,  ( abs  o.  -  ) >.
3729, 33, 36ctp 3655 . . 3  class  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }
3821, 37cun 3163 . 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 1632 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  16395  cnfldbas  16399  cnfldadd  16400  cnfldmul  16401  cnfldcj  16402  cnfldtset  16403  cnfldle  16404  cnfldds  16405
  Copyright terms: Public domain W3C validator