Definition df-cnfld 21427

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 21429, cnfldadd 21432, cnfldmul 21434, cnfldcj 21435, cnfldtset 21436, cnfldle 21437, cnfldds 21438, and cnfldbas 21430. 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 21426	. 2 class ℂfld
2		cnx 17231	. . . . . . 7 class ndx
3		cbs 17247	. . . . . . 7 class Base
4	2, 3	cfv 6523	. . . . . 6 class (Base‘ndx)
5		cc 11073	. . . . . 6 class ℂ
6	4, 5	cop 4590	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17288	. . . . . . 7 class +g
8	2, 7	cfv 6523	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1561	. . . . . . . 8 class 𝑥
12	10	cv 1561	. . . . . . . 8 class 𝑦
13		caddc 11078	. . . . . . . 8 class +
14	11, 12, 13	co 7398	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7400	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4590	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17289	. . . . . . 7 class .r
18	2, 17	cfv 6523	. . . . . 6 class (.r‘ndx)
19		cmul 11080	. . . . . . . 8 class ·
20	11, 12, 19	co 7398	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7400	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4590	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4588	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17290	. . . . . . 7 class *𝑟
25	2, 24	cfv 6523	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15125	. . . . . 6 class ∗
27	25, 26	cop 4590	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4584	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3904	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17294	. . . . . . 7 class TopSet
31	2, 30	cfv 6523	. . . . . 6 class (TopSet‘ndx)
32		cabs 15263	. . . . . . . 8 class abs
33		cmin 11416	. . . . . . . 8 class −
34	32, 33	ccom 5653	. . . . . . 7 class (abs ∘ − )
35		cmopn 21416	. . . . . . 7 class MetOpen
36	34, 35	cfv 6523	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4590	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17295	. . . . . . 7 class le
39	2, 38	cfv 6523	. . . . . 6 class (le‘ndx)
40		cle 11219	. . . . . 6 class ≤
41	39, 40	cop 4590	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17297	. . . . . . 7 class dist
43	2, 42	cfv 6523	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4590	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4588	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17298	. . . . . . 7 class UnifSet
47	2, 46	cfv 6523	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21417	. . . . . . 7 class metUnif
49	34, 48	cfv 6523	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4590	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4584	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3904	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3904	. 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 1562	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  21428  cnfldex  21429  cnfldbas  21430  mpocnfldadd  21431  mpocnfldmul  21433  cnfldcj  21435  cnfldtset  21436  cnfldle  21437  cnfldds  21438  cnfldunif  21439  cnfldfun  21440  cnfldfunALT  21441  cffldtocusgr  29650