Definition df-cnfld 21640

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 21642, cnfldadd 21645, cnfldmul 21647, cnfldcj 21648, cnfldtset 21649, cnfldle 21650, cnfldds 21651, and cnfldbas 21643. 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 21639	. 2 class ℂfld
2		cnx 17332	. . . . . . 7 class ndx
3		cbs 17348	. . . . . . 7 class Base
4	2, 3	cfv 6527	. . . . . 6 class (Base‘ndx)
5		cc 11169	. . . . . 6 class ℂ
6	4, 5	cop 4589	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17389	. . . . . . 7 class +g
8	2, 7	cfv 6527	. . . . . 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 11174	. . . . . . . 8 class +
14	11, 12, 13	co 7408	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7410	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4589	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17390	. . . . . . 7 class .r
18	2, 17	cfv 6527	. . . . . 6 class (.r‘ndx)
19		cmul 11176	. . . . . . . 8 class ·
20	11, 12, 19	co 7408	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7410	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4589	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4587	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17391	. . . . . . 7 class *𝑟
25	2, 24	cfv 6527	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15230	. . . . . 6 class ∗
27	25, 26	cop 4589	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4583	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3896	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17395	. . . . . . 7 class TopSet
31	2, 30	cfv 6527	. . . . . 6 class (TopSet‘ndx)
32		cabs 15368	. . . . . . . 8 class abs
33		cmin 11512	. . . . . . . 8 class −
34	32, 33	ccom 5651	. . . . . . 7 class (abs ∘ − )
35		cmopn 21629	. . . . . . 7 class MetOpen
36	34, 35	cfv 6527	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4589	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17396	. . . . . . 7 class le
39	2, 38	cfv 6527	. . . . . 6 class (le‘ndx)
40		cle 11315	. . . . . 6 class ≤
41	39, 40	cop 4589	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17398	. . . . . . 7 class dist
43	2, 42	cfv 6527	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4589	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4587	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17399	. . . . . . 7 class UnifSet
47	2, 46	cfv 6527	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21630	. . . . . . 7 class metUnif
49	34, 48	cfv 6527	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4589	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4583	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3896	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3896	. 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  21641  cnfldex  21642  cnfldbas  21643  mpocnfldadd  21644  mpocnfldmul  21646  cnfldcj  21648  cnfldtset  21649  cnfldle  21650  cnfldds  21651  cnfldunif  21652  cnfldfun  21653  cnfldfunALT  21654  cffldtocusgr  29961