Definition df-cnfld 21262

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 21264, cnfldadd 21267, cnfldmul 21269, cnfldcj 21270, cnfldtset 21271, cnfldle 21272, cnfldds 21273, and cnfldbas 21265. 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 21261	. 2 class ℂfld
2		cnx 17104	. . . . . . 7 class ndx
3		cbs 17120	. . . . . . 7 class Base
4	2, 3	cfv 6482	. . . . . 6 class (Base‘ndx)
5		cc 11007	. . . . . 6 class ℂ
6	4, 5	cop 4583	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17161	. . . . . . 7 class +g
8	2, 7	cfv 6482	. . . . . 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 11012	. . . . . . . 8 class +
14	11, 12, 13	co 7349	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7351	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4583	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17162	. . . . . . 7 class .r
18	2, 17	cfv 6482	. . . . . 6 class (.r‘ndx)
19		cmul 11014	. . . . . . . 8 class ·
20	11, 12, 19	co 7349	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7351	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4583	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4581	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17163	. . . . . . 7 class *𝑟
25	2, 24	cfv 6482	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15003	. . . . . 6 class ∗
27	25, 26	cop 4583	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4577	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3901	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17167	. . . . . . 7 class TopSet
31	2, 30	cfv 6482	. . . . . 6 class (TopSet‘ndx)
32		cabs 15141	. . . . . . . 8 class abs
33		cmin 11347	. . . . . . . 8 class −
34	32, 33	ccom 5623	. . . . . . 7 class (abs ∘ − )
35		cmopn 21251	. . . . . . 7 class MetOpen
36	34, 35	cfv 6482	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4583	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17168	. . . . . . 7 class le
39	2, 38	cfv 6482	. . . . . 6 class (le‘ndx)
40		cle 11150	. . . . . 6 class ≤
41	39, 40	cop 4583	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17170	. . . . . . 7 class dist
43	2, 42	cfv 6482	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4583	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4581	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17171	. . . . . . 7 class UnifSet
47	2, 46	cfv 6482	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21252	. . . . . . 7 class metUnif
49	34, 48	cfv 6482	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4583	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4577	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3901	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3901	. 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  21263  cnfldex  21264  cnfldbas  21265  mpocnfldadd  21266  mpocnfldmul  21268  cnfldcj  21270  cnfldtset  21271  cnfldle  21272  cnfldds  21273  cnfldunif  21274  cnfldfun  21275  cnfldfunALT  21276  dfcnfldOLD  21277  cffldtocusgr  29396