Definition df-cnfld 21585

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 21587, cnfldadd 21590, cnfldmul 21592, cnfldcj 21593, cnfldtset 21594, cnfldle 21595, cnfldds 21596, and cnfldbas 21588. 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 21584	. 2 class ℂfld
2		cnx 17287	. . . . . . 7 class ndx
3		cbs 17303	. . . . . . 7 class Base
4	2, 3	cfv 6537	. . . . . 6 class (Base‘ndx)
5		cc 11123	. . . . . 6 class ℂ
6	4, 5	cop 4593	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17344	. . . . . . 7 class +g
8	2, 7	cfv 6537	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1569	. . . . . . . 8 class 𝑥
12	10	cv 1569	. . . . . . . 8 class 𝑦
13		caddc 11128	. . . . . . . 8 class +
14	11, 12, 13	co 7416	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7418	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4593	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17345	. . . . . . 7 class .r
18	2, 17	cfv 6537	. . . . . 6 class (.r‘ndx)
19		cmul 11130	. . . . . . . 8 class ·
20	11, 12, 19	co 7416	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7418	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4593	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4591	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17346	. . . . . . 7 class *𝑟
25	2, 24	cfv 6537	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15183	. . . . . 6 class ∗
27	25, 26	cop 4593	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4587	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3900	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17350	. . . . . . 7 class TopSet
31	2, 30	cfv 6537	. . . . . 6 class (TopSet‘ndx)
32		cabs 15321	. . . . . . . 8 class abs
33		cmin 11466	. . . . . . . 8 class −
34	32, 33	ccom 5663	. . . . . . 7 class (abs ∘ − )
35		cmopn 21574	. . . . . . 7 class MetOpen
36	34, 35	cfv 6537	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4593	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17351	. . . . . . 7 class le
39	2, 38	cfv 6537	. . . . . 6 class (le‘ndx)
40		cle 11269	. . . . . 6 class ≤
41	39, 40	cop 4593	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17353	. . . . . . 7 class dist
43	2, 42	cfv 6537	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4593	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4591	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17354	. . . . . . 7 class UnifSet
47	2, 46	cfv 6537	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21575	. . . . . . 7 class metUnif
49	34, 48	cfv 6537	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4593	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4587	. . . 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 1570	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  21586  cnfldex  21587  cnfldbas  21588  mpocnfldadd  21589  mpocnfldmul  21591  cnfldcj  21593  cnfldtset  21594  cnfldle  21595  cnfldds  21596  cnfldunif  21597  cnfldfun  21598  cnfldfunALT  21599  cffldtocusgr  29891