Definition df-cnfld 21532

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 21534, cnfldadd 21537, cnfldmul 21539, cnfldcj 21540, cnfldtset 21541, cnfldle 21542, cnfldds 21543, and cnfldbas 21535. 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 21531	. 2 class ℂfld
2		cnx 17257	. . . . . . 7 class ndx
3		cbs 17273	. . . . . . 7 class Base
4	2, 3	cfv 6536	. . . . . 6 class (Base‘ndx)
5		cc 11102	. . . . . 6 class ℂ
6	4, 5	cop 4595	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17314	. . . . . . 7 class +g
8	2, 7	cfv 6536	. . . . . 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 11107	. . . . . . . 8 class +
14	11, 12, 13	co 7410	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7412	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4595	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17315	. . . . . . 7 class .r
18	2, 17	cfv 6536	. . . . . 6 class (.r‘ndx)
19		cmul 11109	. . . . . . . 8 class ·
20	11, 12, 19	co 7410	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7412	. . . . . 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 17316	. . . . . . 7 class *𝑟
25	2, 24	cfv 6536	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15152	. . . . . 6 class ∗
27	25, 26	cop 4595	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4589	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3903	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17320	. . . . . . 7 class TopSet
31	2, 30	cfv 6536	. . . . . 6 class (TopSet‘ndx)
32		cabs 15290	. . . . . . . 8 class abs
33		cmin 11445	. . . . . . . 8 class −
34	32, 33	ccom 5665	. . . . . . 7 class (abs ∘ − )
35		cmopn 21521	. . . . . . 7 class MetOpen
36	34, 35	cfv 6536	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4595	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17321	. . . . . . 7 class le
39	2, 38	cfv 6536	. . . . . 6 class (le‘ndx)
40		cle 11248	. . . . . 6 class ≤
41	39, 40	cop 4595	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17323	. . . . . . 7 class dist
43	2, 42	cfv 6536	. . . . . 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 17324	. . . . . . 7 class UnifSet
47	2, 46	cfv 6536	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21522	. . . . . . 7 class metUnif
49	34, 48	cfv 6536	. . . . . 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 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 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  21533  cnfldex  21534  cnfldbas  21535  mpocnfldadd  21536  mpocnfldmul  21538  cnfldcj  21540  cnfldtset  21541  cnfldle  21542  cnfldds  21543  cnfldunif  21544  cnfldfun  21545  cnfldfunALT  21546  cffldtocusgr  29806