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 21365
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 21367, cnfldadd 21370, cnfldmul 21372, cnfldcj 21373, cnfldtset 21374, cnfldle 21375, cnfldds 21376, and cnfldbas 21368. 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.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (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 ∘ − ))⟩}))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-cnfld
StepHypRef Expression
1 ccnfld 21364 . 2 class fld
2 cnx 17230 . . . . . . 7 class ndx
3 cbs 17247 . . . . . . 7 class Base
42, 3cfv 6561 . . . . . 6 class (Base‘ndx)
5 cc 11153 . . . . . 6 class
64, 5cop 4632 . . . . 5 class ⟨(Base‘ndx), ℂ⟩
7 cplusg 17297 . . . . . . 7 class +g
82, 7cfv 6561 . . . . . 6 class (+g‘ndx)
9 vx . . . . . . 7 setvar 𝑥
10 vy . . . . . . 7 setvar 𝑦
119cv 1539 . . . . . . . 8 class 𝑥
1210cv 1539 . . . . . . . 8 class 𝑦
13 caddc 11158 . . . . . . . 8 class +
1411, 12, 13co 7431 . . . . . . 7 class (𝑥 + 𝑦)
159, 10, 5, 5, 14cmpo 7433 . . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
168, 15cop 4632 . . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17 cmulr 17298 . . . . . . 7 class .r
182, 17cfv 6561 . . . . . 6 class (.r‘ndx)
19 cmul 11160 . . . . . . . 8 class ·
2011, 12, 19co 7431 . . . . . . 7 class (𝑥 · 𝑦)
219, 10, 5, 5, 20cmpo 7433 . . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
2218, 21cop 4632 . . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
236, 16, 22ctp 4630 . . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24 cstv 17299 . . . . . . 7 class *𝑟
252, 24cfv 6561 . . . . . 6 class (*𝑟‘ndx)
26 ccj 15135 . . . . . 6 class
2725, 26cop 4632 . . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
2827csn 4626 . . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
2923, 28cun 3949 . . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30 cts 17303 . . . . . . 7 class TopSet
312, 30cfv 6561 . . . . . 6 class (TopSet‘ndx)
32 cabs 15273 . . . . . . . 8 class abs
33 cmin 11492 . . . . . . . 8 class
3432, 33ccom 5689 . . . . . . 7 class (abs ∘ − )
35 cmopn 21354 . . . . . . 7 class MetOpen
3634, 35cfv 6561 . . . . . 6 class (MetOpen‘(abs ∘ − ))
3731, 36cop 4632 . . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38 cple 17304 . . . . . . 7 class le
392, 38cfv 6561 . . . . . 6 class (le‘ndx)
40 cle 11296 . . . . . 6 class
4139, 40cop 4632 . . . . 5 class ⟨(le‘ndx), ≤ ⟩
42 cds 17306 . . . . . . 7 class dist
432, 42cfv 6561 . . . . . 6 class (dist‘ndx)
4443, 34cop 4632 . . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
4537, 41, 44ctp 4630 . . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46 cunif 17307 . . . . . . 7 class UnifSet
472, 46cfv 6561 . . . . . 6 class (UnifSet‘ndx)
48 cmetu 21355 . . . . . . 7 class metUnif
4934, 48cfv 6561 . . . . . 6 class (metUnif‘(abs ∘ − ))
5047, 49cop 4632 . . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
5150csn 4626 . . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
5245, 51cun 3949 . . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
5329, 52cun 3949 . 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
541, 53wceq 1540 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  21366  cnfldex  21367  cnfldbas  21368  mpocnfldadd  21369  mpocnfldmul  21371  cnfldcj  21373  cnfldtset  21374  cnfldle  21375  cnfldds  21376  cnfldunif  21377  cnfldfun  21378  cnfldfunALT  21379  dfcnfldOLD  21380  cffldtocusgr  29464
  Copyright terms: Public domain W3C validator