Definition df-cnfld 21314

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 21316, cnfldadd 21319, cnfldmul 21321, cnfldcj 21322, cnfldtset 21323, cnfldle 21324, cnfldds 21325, and cnfldbas 21317. 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 21313	. 2 class ℂfld
2		cnx 17210	. . . . . . 7 class ndx
3		cbs 17226	. . . . . . 7 class Base
4	2, 3	cfv 6530	. . . . . 6 class (Base‘ndx)
5		cc 11125	. . . . . 6 class ℂ
6	4, 5	cop 4607	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17269	. . . . . . 7 class +g
8	2, 7	cfv 6530	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1539	. . . . . . . 8 class 𝑥
12	10	cv 1539	. . . . . . . 8 class 𝑦
13		caddc 11130	. . . . . . . 8 class +
14	11, 12, 13	co 7403	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7405	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4607	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17270	. . . . . . 7 class .r
18	2, 17	cfv 6530	. . . . . 6 class (.r‘ndx)
19		cmul 11132	. . . . . . . 8 class ·
20	11, 12, 19	co 7403	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7405	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4607	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4605	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17271	. . . . . . 7 class *𝑟
25	2, 24	cfv 6530	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15113	. . . . . 6 class ∗
27	25, 26	cop 4607	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4601	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3924	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17275	. . . . . . 7 class TopSet
31	2, 30	cfv 6530	. . . . . 6 class (TopSet‘ndx)
32		cabs 15251	. . . . . . . 8 class abs
33		cmin 11464	. . . . . . . 8 class −
34	32, 33	ccom 5658	. . . . . . 7 class (abs ∘ − )
35		cmopn 21303	. . . . . . 7 class MetOpen
36	34, 35	cfv 6530	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4607	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17276	. . . . . . 7 class le
39	2, 38	cfv 6530	. . . . . 6 class (le‘ndx)
40		cle 11268	. . . . . 6 class ≤
41	39, 40	cop 4607	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17278	. . . . . . 7 class dist
43	2, 42	cfv 6530	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4607	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4605	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17279	. . . . . . 7 class UnifSet
47	2, 46	cfv 6530	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21304	. . . . . . 7 class metUnif
49	34, 48	cfv 6530	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4607	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4601	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3924	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3924	. 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 1540	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  21315  cnfldex  21316  cnfldbas  21317  mpocnfldadd  21318  mpocnfldmul  21320  cnfldcj  21322  cnfldtset  21323  cnfldle  21324  cnfldds  21325  cnfldunif  21326  cnfldfun  21327  cnfldfunALT  21328  dfcnfldOLD  21329  cffldtocusgr  29372