Definition df-cnfld 21349

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 21351, cnfldadd 21354, cnfldmul 21356, cnfldcj 21357, cnfldtset 21358, cnfldle 21359, cnfldds 21360, and cnfldbas 21352. 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 21348	. 2 class ℂfld
2		cnx 17158	. . . . . . 7 class ndx
3		cbs 17174	. . . . . . 7 class Base
4	2, 3	cfv 6494	. . . . . 6 class (Base‘ndx)
5		cc 11031	. . . . . 6 class ℂ
6	4, 5	cop 4574	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17215	. . . . . . 7 class +g
8	2, 7	cfv 6494	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1541	. . . . . . . 8 class 𝑥
12	10	cv 1541	. . . . . . . 8 class 𝑦
13		caddc 11036	. . . . . . . 8 class +
14	11, 12, 13	co 7362	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7364	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4574	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17216	. . . . . . 7 class .r
18	2, 17	cfv 6494	. . . . . 6 class (.r‘ndx)
19		cmul 11038	. . . . . . . 8 class ·
20	11, 12, 19	co 7362	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7364	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4574	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4572	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17217	. . . . . . 7 class *𝑟
25	2, 24	cfv 6494	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15053	. . . . . 6 class ∗
27	25, 26	cop 4574	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4568	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3888	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17221	. . . . . . 7 class TopSet
31	2, 30	cfv 6494	. . . . . 6 class (TopSet‘ndx)
32		cabs 15191	. . . . . . . 8 class abs
33		cmin 11372	. . . . . . . 8 class −
34	32, 33	ccom 5630	. . . . . . 7 class (abs ∘ − )
35		cmopn 21338	. . . . . . 7 class MetOpen
36	34, 35	cfv 6494	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4574	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17222	. . . . . . 7 class le
39	2, 38	cfv 6494	. . . . . 6 class (le‘ndx)
40		cle 11175	. . . . . 6 class ≤
41	39, 40	cop 4574	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17224	. . . . . . 7 class dist
43	2, 42	cfv 6494	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4574	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4572	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17225	. . . . . . 7 class UnifSet
47	2, 46	cfv 6494	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21339	. . . . . . 7 class metUnif
49	34, 48	cfv 6494	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4574	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4568	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3888	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3888	. 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 1542	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  21350  cnfldex  21351  cnfldbas  21352  mpocnfldadd  21353  mpocnfldmul  21355  cnfldcj  21357  cnfldtset  21358  cnfldle  21359  cnfldds  21360  cnfldunif  21361  cnfldfun  21362  cnfldfunALT  21363  dfcnfldOLD  21364  cffldtocusgr  29534