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 19951
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 19953, cnfldadd 19955, cnfldmul 19956, cnfldcj 19957, cnfldtset 19958, cnfldle 19959, cnfldds 19960, and cnfldbas 19954. 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 19950 . 2 class fld
2 cnx 16061 . . . . . . 7 class ndx
3 cbs 16064 . . . . . . 7 class Base
42, 3cfv 6097 . . . . . 6 class (Base‘ndx)
5 cc 10215 . . . . . 6 class
64, 5cop 4376 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 16149 . . . . . . 7 class +g
82, 7cfv 6097 . . . . . 6 class (+g‘ndx)
9 caddc 10220 . . . . . 6 class +
108, 9cop 4376 . . . . 5 class ⟨(+g‘ndx), + ⟩
11 cmulr 16150 . . . . . . 7 class .r
122, 11cfv 6097 . . . . . 6 class (.r‘ndx)
13 cmul 10222 . . . . . 6 class ·
1412, 13cop 4376 . . . . 5 class ⟨(.r‘ndx), · ⟩
156, 10, 14ctp 4374 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16 cstv 16151 . . . . . . 7 class *𝑟
172, 16cfv 6097 . . . . . 6 class (*𝑟‘ndx)
18 ccj 14055 . . . . . 6 class
1917, 18cop 4376 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2019csn 4370 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2115, 20cun 3767 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22 cts 16155 . . . . . . 7 class TopSet
232, 22cfv 6097 . . . . . 6 class (TopSet‘ndx)
24 cabs 14193 . . . . . . . 8 class abs
25 cmin 10547 . . . . . . . 8 class
2624, 25ccom 5315 . . . . . . 7 class (abs ∘ − )
27 cmopn 19940 . . . . . . 7 class MetOpen
2826, 27cfv 6097 . . . . . 6 class (MetOpen‘(abs ∘ − ))
2923, 28cop 4376 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30 cple 16156 . . . . . . 7 class le
312, 30cfv 6097 . . . . . 6 class (le‘ndx)
32 cle 10356 . . . . . 6 class
3331, 32cop 4376 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
34 cds 16158 . . . . . . 7 class dist
352, 34cfv 6097 . . . . . 6 class (dist‘ndx)
3635, 26cop 4376 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
3729, 33, 36ctp 4374 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38 cunif 16159 . . . . . . 7 class UnifSet
392, 38cfv 6097 . . . . . 6 class (UnifSet‘ndx)
40 cmetu 19941 . . . . . . 7 class metUnif
4126, 40cfv 6097 . . . . . 6 class (metUnif‘(abs ∘ − ))
4239, 41cop 4376 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
4342csn 4370 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
4437, 43cun 3767 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
4521, 44cun 3767 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
461, 45wceq 1637 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  19952  cnfldbas  19954  cnfldadd  19955  cnfldmul  19956  cnfldcj  19957  cnfldtset  19958  cnfldle  19959  cnfldds  19960  cnfldunif  19961  cnfldfun  19962  cnfldfunALT  19963  cffldtocusgr  26570
  Copyright terms: Public domain W3C validator