Definition df-cnfld 21314

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 21316, cnfldadd 21319, cnfldmul 21321, cnfldcj 21322, cnfldtset 21323, cnfldle 21324, cnfldds 21325, and cnfldbas 21317. 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 21313	. 2 class ℂfld
2		cnx 17124	. . . . . . 7 class ndx
3		cbs 17140	. . . . . . 7 class Base
4	2, 3	cfv 6493	. . . . . 6 class (Base‘ndx)
5		cc 11028	. . . . . 6 class ℂ
6	4, 5	cop 4587	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17181	. . . . . . 7 class +g
8	2, 7	cfv 6493	. . . . . 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 11033	. . . . . . . 8 class +
14	11, 12, 13	co 7360	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7362	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4587	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17182	. . . . . . 7 class .r
18	2, 17	cfv 6493	. . . . . 6 class (.r‘ndx)
19		cmul 11035	. . . . . . . 8 class ·
20	11, 12, 19	co 7360	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7362	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4587	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4585	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17183	. . . . . . 7 class *𝑟
25	2, 24	cfv 6493	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15023	. . . . . 6 class ∗
27	25, 26	cop 4587	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4581	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3900	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17187	. . . . . . 7 class TopSet
31	2, 30	cfv 6493	. . . . . 6 class (TopSet‘ndx)
32		cabs 15161	. . . . . . . 8 class abs
33		cmin 11368	. . . . . . . 8 class −
34	32, 33	ccom 5629	. . . . . . 7 class (abs ∘ − )
35		cmopn 21303	. . . . . . 7 class MetOpen
36	34, 35	cfv 6493	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4587	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17188	. . . . . . 7 class le
39	2, 38	cfv 6493	. . . . . 6 class (le‘ndx)
40		cle 11171	. . . . . 6 class ≤
41	39, 40	cop 4587	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17190	. . . . . . 7 class dist
43	2, 42	cfv 6493	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4587	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4585	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17191	. . . . . . 7 class UnifSet
47	2, 46	cfv 6493	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21304	. . . . . . 7 class metUnif
49	34, 48	cfv 6493	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4587	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4581	. . . 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 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  21315  cnfldex  21316  cnfldbas  21317  mpocnfldadd  21318  mpocnfldmul  21320  cnfldcj  21322  cnfldtset  21323  cnfldle  21324  cnfldds  21325  cnfldunif  21326  cnfldfun  21327  cnfldfunALT  21328  dfcnfldOLD  21329  cffldtocusgr  29524