Definition df-cnfld 21679

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 21681, cnfldadd 21684, cnfldmul 21686, cnfldcj 21687, cnfldtset 21688, cnfldle 21689, cnfldds 21690, and cnfldbas 21682. 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 21678	. 2 class ℂfld
2		cnx 17371	. . . . . . 7 class ndx
3		cbs 17387	. . . . . . 7 class Base
4	2, 3	cfv 6538	. . . . . 6 class (Base‘ndx)
5		cc 11198	. . . . . 6 class ℂ
6	4, 5	cop 4589	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17428	. . . . . . 7 class +g
8	2, 7	cfv 6538	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1568	. . . . . . . 8 class 𝑥
12	10	cv 1568	. . . . . . . 8 class 𝑦
13		caddc 11203	. . . . . . . 8 class +
14	11, 12, 13	co 7420	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7422	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4589	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17429	. . . . . . 7 class .r
18	2, 17	cfv 6538	. . . . . 6 class (.r‘ndx)
19		cmul 11205	. . . . . . . 8 class ·
20	11, 12, 19	co 7420	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7422	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4589	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4587	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17430	. . . . . . 7 class *𝑟
25	2, 24	cfv 6538	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15263	. . . . . 6 class ∗
27	25, 26	cop 4589	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4583	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 4149	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17434	. . . . . . 7 class TopSet
31	2, 30	cfv 6538	. . . . . 6 class (TopSet‘ndx)
32		cabs 15401	. . . . . . . 8 class abs
33		cmin 11541	. . . . . . . 8 class −
34	32, 33	ccom 5654	. . . . . . 7 class (abs ∘ − )
35		cmopn 21668	. . . . . . 7 class MetOpen
36	34, 35	cfv 6538	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4589	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17435	. . . . . . 7 class le
39	2, 38	cfv 6538	. . . . . 6 class (le‘ndx)
40		cle 11344	. . . . . 6 class ≤
41	39, 40	cop 4589	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17437	. . . . . . 7 class dist
43	2, 42	cfv 6538	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4589	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4587	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17438	. . . . . . 7 class UnifSet
47	2, 46	cfv 6538	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21669	. . . . . . 7 class metUnif
49	34, 48	cfv 6538	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4589	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4583	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 4149	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 4149	. 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 1569	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 used by:  cnfldstr  21680  cnfldex  21681  cnfldbas  21682  mpocnfldadd  21683  mpocnfldmul  21685  cnfldcj  21687  cnfldtset  21688  cnfldle  21689  cnfldds  21690  cnfldunif  21691  cnfldfun  21692  cnfldfunALT  21693  cffldtocusgr  30028