Definition df-cnfld 14978

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ↾_s restriction operator.

The contract of this set is defined entirely by cnfldex 14980, cnfldadd 14983, cnfldmul 14985, cnfldcj 14986, cnfldtset 14987, cnfldle 14988, cnfldds 14989, and cnfldbas 14981. 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 14977	. 2 class ℂfld
2		cnx 13401	. . . . . . 7 class ndx
3		cbs 13404	. . . . . . 7 class Base
4	2, 3	cfv 5377	. . . . . 6 class (Base‘ndx)
5		cc 8178	. . . . . 6 class ℂ
6	4, 5	cop 3712	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13484	. . . . . . 7 class +g
8	2, 7	cfv 5377	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1401	. . . . . . . 8 class 𝑥
12	10	cv 1401	. . . . . . . 8 class 𝑦
13		caddc 8183	. . . . . . . 8 class +
14	11, 12, 13	co 6085	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6087	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3712	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13485	. . . . . . 7 class .r
18	2, 17	cfv 5377	. . . . . 6 class (.r‘ndx)
19		cmul 8185	. . . . . . . 8 class ·
20	11, 12, 19	co 6085	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6087	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3712	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3711	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13486	. . . . . . 7 class *𝑟
25	2, 24	cfv 5377	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11620	. . . . . 6 class ∗
27	25, 26	cop 3712	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3709	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3218	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13490	. . . . . . 7 class TopSet
31	2, 30	cfv 5377	. . . . . 6 class (TopSet‘ndx)
32		cabs 11779	. . . . . . . 8 class abs
33		cmin 8499	. . . . . . . 8 class −
34	32, 33	ccom 4778	. . . . . . 7 class (abs ∘ − )
35		cmopn 14962	. . . . . . 7 class MetOpen
36	34, 35	cfv 5377	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3712	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13491	. . . . . . 7 class le
39	2, 38	cfv 5377	. . . . . 6 class (le‘ndx)
40		cle 8362	. . . . . 6 class ≤
41	39, 40	cop 3712	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13493	. . . . . . 7 class dist
43	2, 42	cfv 5377	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3712	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3711	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13494	. . . . . . 7 class UnifSet
47	2, 46	cfv 5377	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14963	. . . . . . 7 class metUnif
49	34, 48	cfv 5377	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3712	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3709	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3218	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3218	. 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 1402	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  14979  cnfldbas  14981  mpocnfldadd  14982  mpocnfldmul  14984  cnfldcj  14986  cnfldtset  14987  cnfldle  14988  cnfldds  14989