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

Definition df-cnfld 16659
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 16661, cnfldadd 16663, cnfldmul 16664, cnfldcj 16665, cnfldtset 16666, cnfldle 16667, cnfldds 16668, and cnfldbas 16662. 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 16658 . 2  classfld
2 cnx 13421 . . . . . . 7  class  ndx
3 cbs 13424 . . . . . . 7  class  Base
42, 3cfv 5413 . . . . . 6  class  ( Base `  ndx )
5 cc 8944 . . . . . 6  class  CC
64, 5cop 3777 . . . . 5  class  <. ( Base `  ndx ) ,  CC >.
7 cplusg 13484 . . . . . . 7  class  +g
82, 7cfv 5413 . . . . . 6  class  ( +g  ` 
ndx )
9 caddc 8949 . . . . . 6  class  +
108, 9cop 3777 . . . . 5  class  <. ( +g  `  ndx ) ,  +  >.
11 cmulr 13485 . . . . . . 7  class  .r
122, 11cfv 5413 . . . . . 6  class  ( .r
`  ndx )
13 cmul 8951 . . . . . 6  class  x.
1412, 13cop 3777 . . . . 5  class  <. ( .r `  ndx ) ,  x.  >.
156, 10, 14ctp 3776 . . . 4  class  { <. (
Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }
16 cstv 13486 . . . . . . 7  class  * r
172, 16cfv 5413 . . . . . 6  class  ( * r `  ndx )
18 ccj 11856 . . . . . 6  class  *
1917, 18cop 3777 . . . . 5  class  <. (
* r `  ndx ) ,  * >.
2019csn 3774 . . . 4  class  { <. ( * r `  ndx ) ,  * >. }
2115, 20cun 3278 . . 3  class  ( {
<. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( * r `  ndx ) ,  * >. } )
22 cts 13490 . . . . . . 7  class TopSet
232, 22cfv 5413 . . . . . 6  class  (TopSet `  ndx )
24 cabs 11994 . . . . . . . 8  class  abs
25 cmin 9247 . . . . . . . 8  class  -
2624, 25ccom 4841 . . . . . . 7  class  ( abs 
o.  -  )
27 cmopn 16646 . . . . . . 7  class  MetOpen
2826, 27cfv 5413 . . . . . 6  class  ( MetOpen `  ( abs  o.  -  )
)
2923, 28cop 3777 . . . . 5  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >.
30 cple 13491 . . . . . . 7  class  le
312, 30cfv 5413 . . . . . 6  class  ( le
`  ndx )
32 cle 9077 . . . . . 6  class  <_
3331, 32cop 3777 . . . . 5  class  <. ( le `  ndx ) ,  <_  >.
34 cds 13493 . . . . . . 7  class  dist
352, 34cfv 5413 . . . . . 6  class  ( dist `  ndx )
3635, 26cop 3777 . . . . 5  class  <. ( dist `  ndx ) ,  ( abs  o.  -  ) >.
3729, 33, 36ctp 3776 . . . 4  class  { <. (TopSet `  ndx ) ,  (
MetOpen `  ( abs  o.  -  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }
38 cunif 13494 . . . . . . 7  class  UnifSet
392, 38cfv 5413 . . . . . 6  class  ( UnifSet ` 
ndx )
40 cmetu 16648 . . . . . . 7  class metUnif
4126, 40cfv 5413 . . . . . 6  class  (metUnif `  ( abs  o.  -  ) )
4239, 41cop 3777 . . . . 5  class  <. ( UnifSet
`  ndx ) ,  (metUnif `  ( abs  o.  -  ) ) >.
4342csn 3774 . . . 4  class  { <. (
UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. }
4437, 43cun 3278 . . 3  class  ( {
<. (TopSet `  ndx ) ,  ( MetOpen `  ( abs  o. 
-  ) ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( abs  o.  -  ) >. }  u.  { <. ( UnifSet `  ndx ) ,  (metUnif `  ( abs  o. 
-  ) ) >. } )
4521, 44cun 3278 . 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 1649 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  16660  cnfldbas  16662  cnfldadd  16663  cnfldmul  16664  cnfldcj  16665  cnfldtset  16666  cnfldle  16667  cnfldds  16668  cnfldunif  16669
  Copyright terms: Public domain W3C validator