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 19795
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 19797, cnfldadd 19799, cnfldmul 19800, cnfldcj 19801, cnfldtset 19802, cnfldle 19803, cnfldds 19804, and cnfldbas 19798. 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 19794 . 2 class fld
2 cnx 15901 . . . . . . 7 class ndx
3 cbs 15904 . . . . . . 7 class Base
42, 3cfv 5926 . . . . . 6 class (Base‘ndx)
5 cc 9972 . . . . . 6 class
64, 5cop 4216 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 15988 . . . . . . 7 class +g
82, 7cfv 5926 . . . . . 6 class (+g‘ndx)
9 caddc 9977 . . . . . 6 class +
108, 9cop 4216 . . . . 5 class ⟨(+g‘ndx), + ⟩
11 cmulr 15989 . . . . . . 7 class .r
122, 11cfv 5926 . . . . . 6 class (.r‘ndx)
13 cmul 9979 . . . . . 6 class ·
1412, 13cop 4216 . . . . 5 class ⟨(.r‘ndx), · ⟩
156, 10, 14ctp 4214 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16 cstv 15990 . . . . . . 7 class *𝑟
172, 16cfv 5926 . . . . . 6 class (*𝑟‘ndx)
18 ccj 13880 . . . . . 6 class
1917, 18cop 4216 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2019csn 4210 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2115, 20cun 3605 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22 cts 15994 . . . . . . 7 class TopSet
232, 22cfv 5926 . . . . . 6 class (TopSet‘ndx)
24 cabs 14018 . . . . . . . 8 class abs
25 cmin 10304 . . . . . . . 8 class
2624, 25ccom 5147 . . . . . . 7 class (abs ∘ − )
27 cmopn 19784 . . . . . . 7 class MetOpen
2826, 27cfv 5926 . . . . . 6 class (MetOpen‘(abs ∘ − ))
2923, 28cop 4216 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30 cple 15995 . . . . . . 7 class le
312, 30cfv 5926 . . . . . 6 class (le‘ndx)
32 cle 10113 . . . . . 6 class
3331, 32cop 4216 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
34 cds 15997 . . . . . . 7 class dist
352, 34cfv 5926 . . . . . 6 class (dist‘ndx)
3635, 26cop 4216 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
3729, 33, 36ctp 4214 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38 cunif 15998 . . . . . . 7 class UnifSet
392, 38cfv 5926 . . . . . 6 class (UnifSet‘ndx)
40 cmetu 19785 . . . . . . 7 class metUnif
4126, 40cfv 5926 . . . . . 6 class (metUnif‘(abs ∘ − ))
4239, 41cop 4216 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
4342csn 4210 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
4437, 43cun 3605 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
4521, 44cun 3605 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
461, 45wceq 1523 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  19796  cnfldbas  19798  cnfldadd  19799  cnfldmul  19800  cnfldcj  19801  cnfldtset  19802  cnfldle  19803  cnfldds  19804  cnfldunif  19805  cnfldfun  19806  cnfldfunALT  19807  cffldtocusgr  26399
  Copyright terms: Public domain W3C validator