Definition df-cnfld 21353

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 21355, cnfldadd 21358, cnfldmul 21360, cnfldcj 21361, cnfldtset 21362, cnfldle 21363, cnfldds 21364, and cnfldbas 21356. 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 21352	. 2 class ℂfld
2		cnx 17163	. . . . . . 7 class ndx
3		cbs 17179	. . . . . . 7 class Base
4	2, 3	cfv 6498	. . . . . 6 class (Base‘ndx)
5		cc 11036	. . . . . 6 class ℂ
6	4, 5	cop 4573	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17220	. . . . . . 7 class +g
8	2, 7	cfv 6498	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1541	. . . . . . . 8 class 𝑥
12	10	cv 1541	. . . . . . . 8 class 𝑦
13		caddc 11041	. . . . . . . 8 class +
14	11, 12, 13	co 7367	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7369	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4573	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17221	. . . . . . 7 class .r
18	2, 17	cfv 6498	. . . . . 6 class (.r‘ndx)
19		cmul 11043	. . . . . . . 8 class ·
20	11, 12, 19	co 7367	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7369	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4573	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4571	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17222	. . . . . . 7 class *𝑟
25	2, 24	cfv 6498	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15058	. . . . . 6 class ∗
27	25, 26	cop 4573	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4567	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3887	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17226	. . . . . . 7 class TopSet
31	2, 30	cfv 6498	. . . . . 6 class (TopSet‘ndx)
32		cabs 15196	. . . . . . . 8 class abs
33		cmin 11377	. . . . . . . 8 class −
34	32, 33	ccom 5635	. . . . . . 7 class (abs ∘ − )
35		cmopn 21342	. . . . . . 7 class MetOpen
36	34, 35	cfv 6498	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4573	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17227	. . . . . . 7 class le
39	2, 38	cfv 6498	. . . . . 6 class (le‘ndx)
40		cle 11180	. . . . . 6 class ≤
41	39, 40	cop 4573	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17229	. . . . . . 7 class dist
43	2, 42	cfv 6498	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4573	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4571	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17230	. . . . . . 7 class UnifSet
47	2, 46	cfv 6498	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21343	. . . . . . 7 class metUnif
49	34, 48	cfv 6498	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4573	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4567	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3887	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3887	. 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 1542	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  21354  cnfldex  21355  cnfldbas  21356  mpocnfldadd  21357  mpocnfldmul  21359  cnfldcj  21361  cnfldtset  21362  cnfldle  21363  cnfldds  21364  cnfldunif  21365  cnfldfun  21366  cnfldfunALT  21367  cffldtocusgr  29516