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 19516
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 19518, cnfldadd 19520, cnfldmul 19521, cnfldcj 19522, cnfldtset 19523, cnfldle 19524, cnfldds 19525, and cnfldbas 19519. 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 19515 . 2 class fld
2 cnx 15640 . . . . . . 7 class ndx
3 cbs 15643 . . . . . . 7 class Base
42, 3cfv 5789 . . . . . 6 class (Base‘ndx)
5 cc 9790 . . . . . 6 class
64, 5cop 4130 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 15716 . . . . . . 7 class +g
82, 7cfv 5789 . . . . . 6 class (+g‘ndx)
9 caddc 9795 . . . . . 6 class +
108, 9cop 4130 . . . . 5 class ⟨(+g‘ndx), + ⟩
11 cmulr 15717 . . . . . . 7 class .r
122, 11cfv 5789 . . . . . 6 class (.r‘ndx)
13 cmul 9797 . . . . . 6 class ·
1412, 13cop 4130 . . . . 5 class ⟨(.r‘ndx), · ⟩
156, 10, 14ctp 4128 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16 cstv 15718 . . . . . . 7 class *𝑟
172, 16cfv 5789 . . . . . 6 class (*𝑟‘ndx)
18 ccj 13632 . . . . . 6 class
1917, 18cop 4130 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2019csn 4124 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2115, 20cun 3537 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22 cts 15722 . . . . . . 7 class TopSet
232, 22cfv 5789 . . . . . 6 class (TopSet‘ndx)
24 cabs 13770 . . . . . . . 8 class abs
25 cmin 10117 . . . . . . . 8 class
2624, 25ccom 5031 . . . . . . 7 class (abs ∘ − )
27 cmopn 19505 . . . . . . 7 class MetOpen
2826, 27cfv 5789 . . . . . 6 class (MetOpen‘(abs ∘ − ))
2923, 28cop 4130 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30 cple 15723 . . . . . . 7 class le
312, 30cfv 5789 . . . . . 6 class (le‘ndx)
32 cle 9931 . . . . . 6 class
3331, 32cop 4130 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
34 cds 15725 . . . . . . 7 class dist
352, 34cfv 5789 . . . . . 6 class (dist‘ndx)
3635, 26cop 4130 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
3729, 33, 36ctp 4128 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38 cunif 15726 . . . . . . 7 class UnifSet
392, 38cfv 5789 . . . . . 6 class (UnifSet‘ndx)
40 cmetu 19506 . . . . . . 7 class metUnif
4126, 40cfv 5789 . . . . . 6 class (metUnif‘(abs ∘ − ))
4239, 41cop 4130 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
4342csn 4124 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
4437, 43cun 3537 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
4521, 44cun 3537 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
461, 45wceq 1474 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  19517  cnfldbas  19519  cnfldadd  19520  cnfldmul  19521  cnfldcj  19522  cnfldtset  19523  cnfldle  19524  cnfldds  19525  cnfldunif  19526
  Copyright terms: Public domain W3C validator