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 20096
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 20098, cnfldadd 20100, cnfldmul 20101, cnfldcj 20102, cnfldtset 20103, cnfldle 20104, cnfldds 20105, and cnfldbas 20099. 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 20095 . 2 class fld
2 cnx 16476 . . . . . . 7 class ndx
3 cbs 16479 . . . . . . 7 class Base
42, 3cfv 6328 . . . . . 6 class (Base‘ndx)
5 cc 10528 . . . . . 6 class
64, 5cop 4534 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 16561 . . . . . . 7 class +g
82, 7cfv 6328 . . . . . 6 class (+g‘ndx)
9 caddc 10533 . . . . . 6 class +
108, 9cop 4534 . . . . 5 class ⟨(+g‘ndx), + ⟩
11 cmulr 16562 . . . . . . 7 class .r
122, 11cfv 6328 . . . . . 6 class (.r‘ndx)
13 cmul 10535 . . . . . 6 class ·
1412, 13cop 4534 . . . . 5 class ⟨(.r‘ndx), · ⟩
156, 10, 14ctp 4532 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16 cstv 16563 . . . . . . 7 class *𝑟
172, 16cfv 6328 . . . . . 6 class (*𝑟‘ndx)
18 ccj 14451 . . . . . 6 class
1917, 18cop 4534 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2019csn 4528 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2115, 20cun 3882 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22 cts 16567 . . . . . . 7 class TopSet
232, 22cfv 6328 . . . . . 6 class (TopSet‘ndx)
24 cabs 14589 . . . . . . . 8 class abs
25 cmin 10863 . . . . . . . 8 class
2624, 25ccom 5527 . . . . . . 7 class (abs ∘ − )
27 cmopn 20085 . . . . . . 7 class MetOpen
2826, 27cfv 6328 . . . . . 6 class (MetOpen‘(abs ∘ − ))
2923, 28cop 4534 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30 cple 16568 . . . . . . 7 class le
312, 30cfv 6328 . . . . . 6 class (le‘ndx)
32 cle 10669 . . . . . 6 class
3331, 32cop 4534 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
34 cds 16570 . . . . . . 7 class dist
352, 34cfv 6328 . . . . . 6 class (dist‘ndx)
3635, 26cop 4534 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
3729, 33, 36ctp 4532 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38 cunif 16571 . . . . . . 7 class UnifSet
392, 38cfv 6328 . . . . . 6 class (UnifSet‘ndx)
40 cmetu 20086 . . . . . . 7 class metUnif
4126, 40cfv 6328 . . . . . 6 class (metUnif‘(abs ∘ − ))
4239, 41cop 4534 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
4342csn 4528 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
4437, 43cun 3882 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
4521, 44cun 3882 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
461, 45wceq 1538 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  20097  cnfldbas  20099  cnfldadd  20100  cnfldmul  20101  cnfldcj  20102  cnfldtset  20103  cnfldle  20104  cnfldds  20105  cnfldunif  20106  cnfldfun  20107  cnfldfunALT  20108  cffldtocusgr  27241
  Copyright terms: Public domain W3C validator