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

Definition df-cnfld 16373
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 16375, cnfldadd 16379, cnfldmul 16380, cnfldcj 16381, cnfldtset 16382, cnfldle 16383, cnfldds 16384, and cnfldbas 16378. 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 16372 . 2  classfld
2 cnx 13140 . . . . . . 7  class  ndx
3 cbs 13143 . . . . . . 7  class  Base
42, 3cfv 5222 . . . . . 6  class  ( Base `  ndx )
5 cc 8731 . . . . . 6  class  CC
64, 5cop 3645 . . . . 5  class  <. ( Base `  ndx ) ,  CC >.
7 cplusg 13203 . . . . . . 7  class  +g
82, 7cfv 5222 . . . . . 6  class  ( +g  ` 
ndx )
9 caddc 8736 . . . . . 6  class  +
108, 9cop 3645 . . . . 5  class  <. ( +g  `  ndx ) ,  +  >.
11 cmulr 13204 . . . . . . 7  class  .r
122, 11cfv 5222 . . . . . 6  class  ( .r
`  ndx )
13 cmul 8738 . . . . . 6  class  x.
1412, 13cop 3645 . . . . 5  class  <. ( .r `  ndx ) ,  x.  >.
156, 10, 14ctp 3644 . . . 4  class  { <. (
Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }
16 cstv 13205 . . . . . . 7  class  * r
172, 16cfv 5222 . . . . . 6  class  ( * r `  ndx )
18 ccj 11576 . . . . . 6  class  *
1917, 18cop 3645 . . . . 5  class  <. (
* r `  ndx ) ,  * >.
2019csn 3642 . . . 4  class  { <. ( * r `  ndx ) ,  * >. }
2115, 20cun 3152 . . 3  class  ( {
<. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )
22 cts 13209 . . . . . 6  class TopSet
232, 22cfv 5222 . . . . 5  class  (TopSet `  ndx )
24 cabs 11714 . . . . . . 7  class  abs
25 cmin 9033 . . . . . . 7  class  -
2624, 25ccom 4693 . . . . . 6  class  ( abs 
o.  -  )
27 cmopn 16367 . . . . . 6  class  MetOpen
2826, 27cfv 5222 . . . . 5  class  ( MetOpen `  ( abs  o.  -  )
)
2923, 28cop 3645 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >.
30 cple 13210 . . . . . 6  class  le
312, 30cfv 5222 . . . . 5  class  ( le
`  ndx )
32 cle 8864 . . . . 5  class  <_
3331, 32cop 3645 . . . 4  class  <. ( le `  ndx ) ,  <_  >.
34 cds 13212 . . . . . 6  class  dist
352, 34cfv 5222 . . . . 5  class  ( dist `  ndx )
3635, 26cop 3645 . . . 4  class  <. ( dist `  ndx ) ,  ( abs  o.  -  ) >.
3729, 33, 36ctp 3644 . . 3  class  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }
3821, 37cun 3152 . 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 1624 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  16374  cnfldbas  16378  cnfldadd  16379  cnfldmul  16380  cnfldcj  16381  cnfldtset  16382  cnfldle  16383  cnfldds  16384
  Copyright terms: Public domain W3C validator