Definition df-cnfld 21388

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 21390, cnfldadd 21393, cnfldmul 21395, cnfldcj 21396, cnfldtset 21397, cnfldle 21398, cnfldds 21399, and cnfldbas 21391. 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

Step	Hyp	Ref	Expression
1		ccnfld 21387	. 2 class ℂfld
2		cnx 17240	. . . . . . 7 class ndx
3		cbs 17258	. . . . . . 7 class Base
4	2, 3	cfv 6573	. . . . . 6 class (Base‘ndx)
5		cc 11182	. . . . . 6 class ℂ
6	4, 5	cop 4654	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17311	. . . . . . 7 class +g
8	2, 7	cfv 6573	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1536	. . . . . . . 8 class 𝑥
12	10	cv 1536	. . . . . . . 8 class 𝑦
13		caddc 11187	. . . . . . . 8 class +
14	11, 12, 13	co 7448	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7450	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4654	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17312	. . . . . . 7 class .r
18	2, 17	cfv 6573	. . . . . 6 class (.r‘ndx)
19		cmul 11189	. . . . . . . 8 class ·
20	11, 12, 19	co 7448	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7450	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4654	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4652	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17313	. . . . . . 7 class *𝑟
25	2, 24	cfv 6573	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15145	. . . . . 6 class ∗
27	25, 26	cop 4654	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4648	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3974	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17317	. . . . . . 7 class TopSet
31	2, 30	cfv 6573	. . . . . 6 class (TopSet‘ndx)
32		cabs 15283	. . . . . . . 8 class abs
33		cmin 11520	. . . . . . . 8 class −
34	32, 33	ccom 5704	. . . . . . 7 class (abs ∘ − )
35		cmopn 21377	. . . . . . 7 class MetOpen
36	34, 35	cfv 6573	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4654	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17318	. . . . . . 7 class le
39	2, 38	cfv 6573	. . . . . 6 class (le‘ndx)
40		cle 11325	. . . . . 6 class ≤
41	39, 40	cop 4654	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17320	. . . . . . 7 class dist
43	2, 42	cfv 6573	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4654	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4652	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17321	. . . . . . 7 class UnifSet
47	2, 46	cfv 6573	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21378	. . . . . . 7 class metUnif
49	34, 48	cfv 6573	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4654	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4648	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3974	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3974	. 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
54	1, 53	wceq 1537	1 wff ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))

This definition is referenced by:  cnfldstr  21389  cnfldex  21390  cnfldbas  21391  mpocnfldadd  21392  mpocnfldmul  21394  cnfldcj  21396  cnfldtset  21397  cnfldle  21398  cnfldds  21399  cnfldunif  21400  cnfldfun  21401  cnfldfunALT  21402  dfcnfldOLD  21403  cffldtocusgr  29482