Definition df-cnfld 14896

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 14898, cnfldadd 14901, cnfldmul 14903, cnfldcj 14904, cnfldtset 14905, cnfldle 14906, cnfldds 14907, and cnfldbas 14899. 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 14895	. 2 class ℂfld
2		cnx 13351	. . . . . . 7 class ndx
3		cbs 13354	. . . . . . 7 class Base
4	2, 3	cfv 5377	. . . . . 6 class (Base‘ndx)
5		cc 8177	. . . . . 6 class ℂ
6	4, 5	cop 3712	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13433	. . . . . . 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 8182	. . . . . . . 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 13434	. . . . . . 7 class .r
18	2, 17	cfv 5377	. . . . . 6 class (.r‘ndx)
19		cmul 8184	. . . . . . . 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 13435	. . . . . . 7 class *𝑟
25	2, 24	cfv 5377	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11606	. . . . . 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 13439	. . . . . . 7 class TopSet
31	2, 30	cfv 5377	. . . . . 6 class (TopSet‘ndx)
32		cabs 11765	. . . . . . . 8 class abs
33		cmin 8497	. . . . . . . 8 class −
34	32, 33	ccom 4778	. . . . . . 7 class (abs ∘ − )
35		cmopn 14880	. . . . . . 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 13440	. . . . . . 7 class le
39	2, 38	cfv 5377	. . . . . 6 class (le‘ndx)
40		cle 8361	. . . . . 6 class ≤
41	39, 40	cop 3712	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13442	. . . . . . 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 13443	. . . . . . 7 class UnifSet
47	2, 46	cfv 5377	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14881	. . . . . . 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  14897  cnfldbas  14899  mpocnfldadd  14900  mpocnfldmul  14902  cnfldcj  14904  cnfldtset  14905  cnfldle  14906  cnfldds  14907