Definition df-cnfld 14113

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 14115, cnfldadd 14118, cnfldmul 14120, cnfldcj 14121, cnfldtset 14122, cnfldle 14123, cnfldds 14124, and cnfldbas 14116. 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 14112	. 2 class ℂfld
2		cnx 12675	. . . . . . 7 class ndx
3		cbs 12678	. . . . . . 7 class Base
4	2, 3	cfv 5258	. . . . . 6 class (Base‘ndx)
5		cc 7877	. . . . . 6 class ℂ
6	4, 5	cop 3625	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12755	. . . . . . 7 class +g
8	2, 7	cfv 5258	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1363	. . . . . . . 8 class 𝑥
12	10	cv 1363	. . . . . . . 8 class 𝑦
13		caddc 7882	. . . . . . . 8 class +
14	11, 12, 13	co 5922	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 5924	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3625	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 12756	. . . . . . 7 class .r
18	2, 17	cfv 5258	. . . . . 6 class (.r‘ndx)
19		cmul 7884	. . . . . . . 8 class ·
20	11, 12, 19	co 5922	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 5924	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3625	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3624	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 12757	. . . . . . 7 class *𝑟
25	2, 24	cfv 5258	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11004	. . . . . 6 class ∗
27	25, 26	cop 3625	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3622	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3155	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 12761	. . . . . . 7 class TopSet
31	2, 30	cfv 5258	. . . . . 6 class (TopSet‘ndx)
32		cabs 11162	. . . . . . . 8 class abs
33		cmin 8197	. . . . . . . 8 class −
34	32, 33	ccom 4667	. . . . . . 7 class (abs ∘ − )
35		cmopn 14097	. . . . . . 7 class MetOpen
36	34, 35	cfv 5258	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3625	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 12762	. . . . . . 7 class le
39	2, 38	cfv 5258	. . . . . 6 class (le‘ndx)
40		cle 8062	. . . . . 6 class ≤
41	39, 40	cop 3625	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 12764	. . . . . . 7 class dist
43	2, 42	cfv 5258	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3625	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3624	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 12765	. . . . . . 7 class UnifSet
47	2, 46	cfv 5258	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14098	. . . . . . 7 class metUnif
49	34, 48	cfv 5258	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3625	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3622	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3155	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3155	. 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 1364	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  14114  cnfldbas  14116  mpocnfldadd  14117  mpocnfldmul  14119  cnfldcj  14121  cnfldtset  14122  cnfldle  14123  cnfldds  14124