Definition df-cnfld 21382

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 21384, cnfldadd 21387, cnfldmul 21389, cnfldcj 21390, cnfldtset 21391, cnfldle 21392, cnfldds 21393, and cnfldbas 21385. 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 21381	. 2 class ℂfld
2		cnx 17226	. . . . . . 7 class ndx
3		cbs 17244	. . . . . . 7 class Base
4	2, 3	cfv 6562	. . . . . 6 class (Base‘ndx)
5		cc 11150	. . . . . 6 class ℂ
6	4, 5	cop 4636	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17297	. . . . . . 7 class +g
8	2, 7	cfv 6562	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1535	. . . . . . . 8 class 𝑥
12	10	cv 1535	. . . . . . . 8 class 𝑦
13		caddc 11155	. . . . . . . 8 class +
14	11, 12, 13	co 7430	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7432	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4636	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17298	. . . . . . 7 class .r
18	2, 17	cfv 6562	. . . . . 6 class (.r‘ndx)
19		cmul 11157	. . . . . . . 8 class ·
20	11, 12, 19	co 7430	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7432	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4636	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4634	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17299	. . . . . . 7 class *𝑟
25	2, 24	cfv 6562	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15131	. . . . . 6 class ∗
27	25, 26	cop 4636	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4630	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3960	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17303	. . . . . . 7 class TopSet
31	2, 30	cfv 6562	. . . . . 6 class (TopSet‘ndx)
32		cabs 15269	. . . . . . . 8 class abs
33		cmin 11489	. . . . . . . 8 class −
34	32, 33	ccom 5692	. . . . . . 7 class (abs ∘ − )
35		cmopn 21371	. . . . . . 7 class MetOpen
36	34, 35	cfv 6562	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4636	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17304	. . . . . . 7 class le
39	2, 38	cfv 6562	. . . . . 6 class (le‘ndx)
40		cle 11293	. . . . . 6 class ≤
41	39, 40	cop 4636	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17306	. . . . . . 7 class dist
43	2, 42	cfv 6562	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4636	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4634	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17307	. . . . . . 7 class UnifSet
47	2, 46	cfv 6562	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21372	. . . . . . 7 class metUnif
49	34, 48	cfv 6562	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4636	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4630	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3960	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3960	. 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 1536	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  21383  cnfldex  21384  cnfldbas  21385  mpocnfldadd  21386  mpocnfldmul  21388  cnfldcj  21390  cnfldtset  21391  cnfldle  21392  cnfldds  21393  cnfldunif  21394  cnfldfun  21395  cnfldfunALT  21396  dfcnfldOLD  21397  cffldtocusgr  29478