Definition df-cnfld 21280

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 21282, cnfldadd 21285, cnfldmul 21287, cnfldcj 21288, cnfldtset 21289, cnfldle 21290, cnfldds 21291, and cnfldbas 21283. 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 21279	. 2 class ℂfld
2		cnx 17122	. . . . . . 7 class ndx
3		cbs 17138	. . . . . . 7 class Base
4	2, 3	cfv 6486	. . . . . 6 class (Base‘ndx)
5		cc 11026	. . . . . 6 class ℂ
6	4, 5	cop 4585	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17179	. . . . . . 7 class +g
8	2, 7	cfv 6486	. . . . . 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 11031	. . . . . . . 8 class +
14	11, 12, 13	co 7353	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7355	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4585	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17180	. . . . . . 7 class .r
18	2, 17	cfv 6486	. . . . . 6 class (.r‘ndx)
19		cmul 11033	. . . . . . . 8 class ·
20	11, 12, 19	co 7353	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7355	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4585	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4583	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17181	. . . . . . 7 class *𝑟
25	2, 24	cfv 6486	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15021	. . . . . 6 class ∗
27	25, 26	cop 4585	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4579	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3903	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17185	. . . . . . 7 class TopSet
31	2, 30	cfv 6486	. . . . . 6 class (TopSet‘ndx)
32		cabs 15159	. . . . . . . 8 class abs
33		cmin 11365	. . . . . . . 8 class −
34	32, 33	ccom 5627	. . . . . . 7 class (abs ∘ − )
35		cmopn 21269	. . . . . . 7 class MetOpen
36	34, 35	cfv 6486	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4585	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17186	. . . . . . 7 class le
39	2, 38	cfv 6486	. . . . . 6 class (le‘ndx)
40		cle 11169	. . . . . 6 class ≤
41	39, 40	cop 4585	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17188	. . . . . . 7 class dist
43	2, 42	cfv 6486	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4585	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4583	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17189	. . . . . . 7 class UnifSet
47	2, 46	cfv 6486	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21270	. . . . . . 7 class metUnif
49	34, 48	cfv 6486	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4585	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4579	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3903	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3903	. 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  21281  cnfldex  21282  cnfldbas  21283  mpocnfldadd  21284  mpocnfldmul  21286  cnfldcj  21288  cnfldtset  21289  cnfldle  21290  cnfldds  21291  cnfldunif  21292  cnfldfun  21293  cnfldfunALT  21294  dfcnfldOLD  21295  cffldtocusgr  29410