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 20476
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 20478, cnfldadd 20480, cnfldmul 20481, cnfldcj 20482, cnfldtset 20483, cnfldle 20484, cnfldds 20485, and cnfldbas 20479. 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 20475 . 2 class fld
2 cnx 16470 . . . . . . 7 class ndx
3 cbs 16473 . . . . . . 7 class Base
42, 3cfv 6349 . . . . . 6 class (Base‘ndx)
5 cc 10524 . . . . . 6 class
64, 5cop 4565 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 16555 . . . . . . 7 class +g
82, 7cfv 6349 . . . . . 6 class (+g‘ndx)
9 caddc 10529 . . . . . 6 class +
108, 9cop 4565 . . . . 5 class ⟨(+g‘ndx), + ⟩
11 cmulr 16556 . . . . . . 7 class .r
122, 11cfv 6349 . . . . . 6 class (.r‘ndx)
13 cmul 10531 . . . . . 6 class ·
1412, 13cop 4565 . . . . 5 class ⟨(.r‘ndx), · ⟩
156, 10, 14ctp 4563 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16 cstv 16557 . . . . . . 7 class *𝑟
172, 16cfv 6349 . . . . . 6 class (*𝑟‘ndx)
18 ccj 14445 . . . . . 6 class
1917, 18cop 4565 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2019csn 4559 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2115, 20cun 3933 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22 cts 16561 . . . . . . 7 class TopSet
232, 22cfv 6349 . . . . . 6 class (TopSet‘ndx)
24 cabs 14583 . . . . . . . 8 class abs
25 cmin 10859 . . . . . . . 8 class
2624, 25ccom 5553 . . . . . . 7 class (abs ∘ − )
27 cmopn 20465 . . . . . . 7 class MetOpen
2826, 27cfv 6349 . . . . . 6 class (MetOpen‘(abs ∘ − ))
2923, 28cop 4565 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30 cple 16562 . . . . . . 7 class le
312, 30cfv 6349 . . . . . 6 class (le‘ndx)
32 cle 10665 . . . . . 6 class
3331, 32cop 4565 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
34 cds 16564 . . . . . . 7 class dist
352, 34cfv 6349 . . . . . 6 class (dist‘ndx)
3635, 26cop 4565 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
3729, 33, 36ctp 4563 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38 cunif 16565 . . . . . . 7 class UnifSet
392, 38cfv 6349 . . . . . 6 class (UnifSet‘ndx)
40 cmetu 20466 . . . . . . 7 class metUnif
4126, 40cfv 6349 . . . . . 6 class (metUnif‘(abs ∘ − ))
4239, 41cop 4565 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
4342csn 4559 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
4437, 43cun 3933 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
4521, 44cun 3933 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
461, 45wceq 1528 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  20477  cnfldbas  20479  cnfldadd  20480  cnfldmul  20481  cnfldcj  20482  cnfldtset  20483  cnfldle  20484  cnfldds  20485  cnfldunif  20486  cnfldfun  20487  cnfldfunALT  20488  cffldtocusgr  27157
  Copyright terms: Public domain W3C validator