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

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

The contract of this set is defined entirely by cnfldex 19570, cnfldadd 19572, cnfldmul 19573, cnfldcj 19574, cnfldtset 19575, cnfldle 19576, cnfldds 19577, and cnfldbas 19571. 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), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))

Detailed syntax breakdown of Definition df-cnfld
StepHypRef Expression
1 ccnfld 19567 . 2 class fld
2 cnx 15692 . . . . . . 7 class ndx
3 cbs 15695 . . . . . . 7 class Base
42, 3cfv 5804 . . . . . 6 class (Base‘ndx)
5 cc 9813 . . . . . 6 class
64, 5cop 4131 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 15768 . . . . . . 7 class +g
82, 7cfv 5804 . . . . . 6 class (+g‘ndx)
9 caddc 9818 . . . . . 6 class +
108, 9cop 4131 . . . . 5 class ⟨(+g‘ndx), + ⟩
11 cmulr 15769 . . . . . . 7 class .r
122, 11cfv 5804 . . . . . 6 class (.r‘ndx)
13 cmul 9820 . . . . . 6 class ·
1412, 13cop 4131 . . . . 5 class ⟨(.r‘ndx), · ⟩
156, 10, 14ctp 4129 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16 cstv 15770 . . . . . . 7 class *𝑟
172, 16cfv 5804 . . . . . 6 class (*𝑟‘ndx)
18 ccj 13684 . . . . . 6 class
1917, 18cop 4131 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2019csn 4125 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2115, 20cun 3538 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22 cts 15774 . . . . . . 7 class TopSet
232, 22cfv 5804 . . . . . 6 class (TopSet‘ndx)
24 cabs 13822 . . . . . . . 8 class abs
25 cmin 10145 . . . . . . . 8 class
2624, 25ccom 5042 . . . . . . 7 class (abs ∘ − )
27 cmopn 19557 . . . . . . 7 class MetOpen
2826, 27cfv 5804 . . . . . 6 class (MetOpen‘(abs ∘ − ))
2923, 28cop 4131 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30 cple 15775 . . . . . . 7 class le
312, 30cfv 5804 . . . . . 6 class (le‘ndx)
32 cle 9954 . . . . . 6 class
3331, 32cop 4131 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
34 cds 15777 . . . . . . 7 class dist
352, 34cfv 5804 . . . . . 6 class (dist‘ndx)
3635, 26cop 4131 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
3729, 33, 36ctp 4129 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38 cunif 15778 . . . . . . 7 class UnifSet
392, 38cfv 5804 . . . . . 6 class (UnifSet‘ndx)
40 cmetu 19558 . . . . . . 7 class metUnif
4126, 40cfv 5804 . . . . . 6 class (metUnif‘(abs ∘ − ))
4239, 41cop 4131 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
4342csn 4125 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
4437, 43cun 3538 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
4521, 44cun 3538 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
461, 45wceq 1475 1 wff fld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
Colors of variables: wff setvar class
This definition is referenced by:  cnfldstr  19569  cnfldbas  19571  cnfldadd  19572  cnfldmul  19573  cnfldcj  19574  cnfldtset  19575  cnfldle  19576  cnfldds  19577  cnfldunif  19578
  Copyright terms: Public domain W3C validator