Definition df-cnfld 21265

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 21267, cnfldadd 21270, cnfldmul 21272, cnfldcj 21273, cnfldtset 21274, cnfldle 21275, cnfldds 21276, and cnfldbas 21268. 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 21264	. 2 class ℂfld
2		cnx 17163	. . . . . . 7 class ndx
3		cbs 17179	. . . . . . 7 class Base
4	2, 3	cfv 6511	. . . . . 6 class (Base‘ndx)
5		cc 11066	. . . . . 6 class ℂ
6	4, 5	cop 4595	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17220	. . . . . . 7 class +g
8	2, 7	cfv 6511	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1539	. . . . . . . 8 class 𝑥
12	10	cv 1539	. . . . . . . 8 class 𝑦
13		caddc 11071	. . . . . . . 8 class +
14	11, 12, 13	co 7387	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7389	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4595	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17221	. . . . . . 7 class .r
18	2, 17	cfv 6511	. . . . . 6 class (.r‘ndx)
19		cmul 11073	. . . . . . . 8 class ·
20	11, 12, 19	co 7387	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7389	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4595	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4593	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17222	. . . . . . 7 class *𝑟
25	2, 24	cfv 6511	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15062	. . . . . 6 class ∗
27	25, 26	cop 4595	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4589	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3912	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17226	. . . . . . 7 class TopSet
31	2, 30	cfv 6511	. . . . . 6 class (TopSet‘ndx)
32		cabs 15200	. . . . . . . 8 class abs
33		cmin 11405	. . . . . . . 8 class −
34	32, 33	ccom 5642	. . . . . . 7 class (abs ∘ − )
35		cmopn 21254	. . . . . . 7 class MetOpen
36	34, 35	cfv 6511	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4595	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17227	. . . . . . 7 class le
39	2, 38	cfv 6511	. . . . . 6 class (le‘ndx)
40		cle 11209	. . . . . 6 class ≤
41	39, 40	cop 4595	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17229	. . . . . . 7 class dist
43	2, 42	cfv 6511	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4595	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4593	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17230	. . . . . . 7 class UnifSet
47	2, 46	cfv 6511	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21255	. . . . . . 7 class metUnif
49	34, 48	cfv 6511	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4595	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4589	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3912	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3912	. 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 1540	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  21266  cnfldex  21267  cnfldbas  21268  mpocnfldadd  21269  mpocnfldmul  21271  cnfldcj  21273  cnfldtset  21274  cnfldle  21275  cnfldds  21276  cnfldunif  21277  cnfldfun  21278  cnfldfunALT  21279  dfcnfldOLD  21280  cffldtocusgr  29374