Definition df-cnfld 14189

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 14191, cnfldadd 14194, cnfldmul 14196, cnfldcj 14197, cnfldtset 14198, cnfldle 14199, cnfldds 14200, and cnfldbas 14192. 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 14188	. 2 class ℂfld
2		cnx 12700	. . . . . . 7 class ndx
3		cbs 12703	. . . . . . 7 class Base
4	2, 3	cfv 5259	. . . . . 6 class (Base‘ndx)
5		cc 7894	. . . . . 6 class ℂ
6	4, 5	cop 3626	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12780	. . . . . . 7 class +g
8	2, 7	cfv 5259	. . . . . 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 7899	. . . . . . . 8 class +
14	11, 12, 13	co 5925	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 5927	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3626	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 12781	. . . . . . 7 class .r
18	2, 17	cfv 5259	. . . . . 6 class (.r‘ndx)
19		cmul 7901	. . . . . . . 8 class ·
20	11, 12, 19	co 5925	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 5927	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3626	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3625	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 12782	. . . . . . 7 class *𝑟
25	2, 24	cfv 5259	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11021	. . . . . 6 class ∗
27	25, 26	cop 3626	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3623	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3155	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 12786	. . . . . . 7 class TopSet
31	2, 30	cfv 5259	. . . . . 6 class (TopSet‘ndx)
32		cabs 11179	. . . . . . . 8 class abs
33		cmin 8214	. . . . . . . 8 class −
34	32, 33	ccom 4668	. . . . . . 7 class (abs ∘ − )
35		cmopn 14173	. . . . . . 7 class MetOpen
36	34, 35	cfv 5259	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3626	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 12787	. . . . . . 7 class le
39	2, 38	cfv 5259	. . . . . 6 class (le‘ndx)
40		cle 8079	. . . . . 6 class ≤
41	39, 40	cop 3626	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 12789	. . . . . . 7 class dist
43	2, 42	cfv 5259	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3626	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3625	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 12790	. . . . . . 7 class UnifSet
47	2, 46	cfv 5259	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14174	. . . . . . 7 class metUnif
49	34, 48	cfv 5259	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3626	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3623	. . . 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  14190  cnfldbas  14192  mpocnfldadd  14193  mpocnfldmul  14195  cnfldcj  14197  cnfldtset  14198  cnfldle  14199  cnfldds  14200