Definition df-cnfld 21301

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 21303, cnfldadd 21306, cnfldmul 21308, cnfldcj 21309, cnfldtset 21310, cnfldle 21311, cnfldds 21312, and cnfldbas 21304. 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 21300	. 2 class ℂfld
2		cnx 17111	. . . . . . 7 class ndx
3		cbs 17127	. . . . . . 7 class Base
4	2, 3	cfv 6489	. . . . . 6 class (Base‘ndx)
5		cc 11015	. . . . . 6 class ℂ
6	4, 5	cop 4583	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17168	. . . . . . 7 class +g
8	2, 7	cfv 6489	. . . . . 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 11020	. . . . . . . 8 class +
14	11, 12, 13	co 7355	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7357	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4583	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17169	. . . . . . 7 class .r
18	2, 17	cfv 6489	. . . . . 6 class (.r‘ndx)
19		cmul 11022	. . . . . . . 8 class ·
20	11, 12, 19	co 7355	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7357	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4583	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4581	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17170	. . . . . . 7 class *𝑟
25	2, 24	cfv 6489	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15010	. . . . . 6 class ∗
27	25, 26	cop 4583	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4577	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3896	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17174	. . . . . . 7 class TopSet
31	2, 30	cfv 6489	. . . . . 6 class (TopSet‘ndx)
32		cabs 15148	. . . . . . . 8 class abs
33		cmin 11355	. . . . . . . 8 class −
34	32, 33	ccom 5625	. . . . . . 7 class (abs ∘ − )
35		cmopn 21290	. . . . . . 7 class MetOpen
36	34, 35	cfv 6489	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4583	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17175	. . . . . . 7 class le
39	2, 38	cfv 6489	. . . . . 6 class (le‘ndx)
40		cle 11158	. . . . . 6 class ≤
41	39, 40	cop 4583	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17177	. . . . . . 7 class dist
43	2, 42	cfv 6489	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4583	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4581	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17178	. . . . . . 7 class UnifSet
47	2, 46	cfv 6489	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21291	. . . . . . 7 class metUnif
49	34, 48	cfv 6489	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4583	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4577	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3896	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3896	. 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  21302  cnfldex  21303  cnfldbas  21304  mpocnfldadd  21305  mpocnfldmul  21307  cnfldcj  21309  cnfldtset  21310  cnfldle  21311  cnfldds  21312  cnfldunif  21313  cnfldfun  21314  cnfldfunALT  21315  dfcnfldOLD  21316  cffldtocusgr  29446