Definition df-cnfld 21706

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 21708, cnfldadd 21711, cnfldmul 21713, cnfldcj 21714, cnfldtset 21715, cnfldle 21716, cnfldds 21717, and cnfldbas 21709. 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 21705	. 2 class ℂfld
2		cnx 17397	. . . . . . 7 class ndx
3		cbs 17413	. . . . . . 7 class Base
4	2, 3	cfv 6555	. . . . . 6 class (Base‘ndx)
5		cc 11222	. . . . . 6 class ℂ
6	4, 5	cop 4838	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17454	. . . . . . 7 class +g
8	2, 7	cfv 6555	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1569	. . . . . . . 8 class 𝑥
12	10	cv 1569	. . . . . . . 8 class 𝑦
13		caddc 11227	. . . . . . . 8 class +
14	11, 12, 13	co 7440	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7442	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4838	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17455	. . . . . . 7 class .r
18	2, 17	cfv 6555	. . . . . 6 class (.r‘ndx)
19		cmul 11229	. . . . . . . 8 class ·
20	11, 12, 19	co 7440	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7442	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4838	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4592	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17456	. . . . . . 7 class *𝑟
25	2, 24	cfv 6555	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15289	. . . . . 6 class ∗
27	25, 26	cop 4838	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4588	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 4152	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17460	. . . . . . 7 class TopSet
31	2, 30	cfv 6555	. . . . . 6 class (TopSet‘ndx)
32		cabs 15427	. . . . . . . 8 class abs
33		cmin 11565	. . . . . . . 8 class −
34	32, 33	ccom 5659	. . . . . . 7 class (abs ∘ − )
35		cmopn 21695	. . . . . . 7 class MetOpen
36	34, 35	cfv 6555	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4838	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17461	. . . . . . 7 class le
39	2, 38	cfv 6555	. . . . . 6 class (le‘ndx)
40		cle 11368	. . . . . 6 class ≤
41	39, 40	cop 4838	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17463	. . . . . . 7 class dist
43	2, 42	cfv 6555	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4838	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4592	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17464	. . . . . . 7 class UnifSet
47	2, 46	cfv 6555	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21696	. . . . . . 7 class metUnif
49	34, 48	cfv 6555	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4838	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4588	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 4152	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 4152	. 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 1570	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  21707  cnfldex  21708  cnfldbas  21709  mpocnfldadd  21710  mpocnfldmul  21712  cnfldcj  21714  cnfldtset  21715  cnfldle  21716  cnfldds  21717  cnfldunif  21718  cnfldfun  21719  cnfldfunALT  21720  cffldtocusgr  30055