Definition df-cnfld 21293

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 21295, cnfldadd 21298, cnfldmul 21300, cnfldcj 21301, cnfldtset 21302, cnfldle 21303, cnfldds 21304, and cnfldbas 21296. 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 21292	. 2 class ℂfld
2		cnx 17104	. . . . . . 7 class ndx
3		cbs 17120	. . . . . . 7 class Base
4	2, 3	cfv 6481	. . . . . 6 class (Base‘ndx)
5		cc 11004	. . . . . 6 class ℂ
6	4, 5	cop 4582	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17161	. . . . . . 7 class +g
8	2, 7	cfv 6481	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1540	. . . . . . . 8 class 𝑥
12	10	cv 1540	. . . . . . . 8 class 𝑦
13		caddc 11009	. . . . . . . 8 class +
14	11, 12, 13	co 7346	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7348	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4582	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17162	. . . . . . 7 class .r
18	2, 17	cfv 6481	. . . . . 6 class (.r‘ndx)
19		cmul 11011	. . . . . . . 8 class ·
20	11, 12, 19	co 7346	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7348	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4582	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4580	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17163	. . . . . . 7 class *𝑟
25	2, 24	cfv 6481	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15003	. . . . . 6 class ∗
27	25, 26	cop 4582	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4576	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3900	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17167	. . . . . . 7 class TopSet
31	2, 30	cfv 6481	. . . . . 6 class (TopSet‘ndx)
32		cabs 15141	. . . . . . . 8 class abs
33		cmin 11344	. . . . . . . 8 class −
34	32, 33	ccom 5620	. . . . . . 7 class (abs ∘ − )
35		cmopn 21282	. . . . . . 7 class MetOpen
36	34, 35	cfv 6481	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4582	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17168	. . . . . . 7 class le
39	2, 38	cfv 6481	. . . . . 6 class (le‘ndx)
40		cle 11147	. . . . . 6 class ≤
41	39, 40	cop 4582	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17170	. . . . . . 7 class dist
43	2, 42	cfv 6481	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4582	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4580	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17171	. . . . . . 7 class UnifSet
47	2, 46	cfv 6481	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21283	. . . . . . 7 class metUnif
49	34, 48	cfv 6481	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4582	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4576	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3900	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3900	. 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 1541	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  21294  cnfldex  21295  cnfldbas  21296  mpocnfldadd  21297  mpocnfldmul  21299  cnfldcj  21301  cnfldtset  21302  cnfldle  21303  cnfldds  21304  cnfldunif  21305  cnfldfun  21306  cnfldfunALT  21307  dfcnfldOLD  21308  cffldtocusgr  29426