Definition df-cnfld 21352

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 21354, cnfldadd 21357, cnfldmul 21359, cnfldcj 21360, cnfldtset 21361, cnfldle 21362, cnfldds 21363, and cnfldbas 21355. 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 21351	. 2 class ℂfld
2		cnx 17158	. . . . . . 7 class ndx
3		cbs 17174	. . . . . . 7 class Base
4	2, 3	cfv 6489	. . . . . 6 class (Base‘ndx)
5		cc 11031	. . . . . 6 class ℂ
6	4, 5	cop 4564	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17215	. . . . . . 7 class +g
8	2, 7	cfv 6489	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1547	. . . . . . . 8 class 𝑥
12	10	cv 1547	. . . . . . . 8 class 𝑦
13		caddc 11036	. . . . . . . 8 class +
14	11, 12, 13	co 7360	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7362	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4564	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17216	. . . . . . 7 class .r
18	2, 17	cfv 6489	. . . . . 6 class (.r‘ndx)
19		cmul 11038	. . . . . . . 8 class ·
20	11, 12, 19	co 7360	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7362	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4564	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4562	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17217	. . . . . . 7 class *𝑟
25	2, 24	cfv 6489	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15053	. . . . . 6 class ∗
27	25, 26	cop 4564	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4558	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3883	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17221	. . . . . . 7 class TopSet
31	2, 30	cfv 6489	. . . . . 6 class (TopSet‘ndx)
32		cabs 15191	. . . . . . . 8 class abs
33		cmin 11372	. . . . . . . 8 class −
34	32, 33	ccom 5625	. . . . . . 7 class (abs ∘ − )
35		cmopn 21341	. . . . . . 7 class MetOpen
36	34, 35	cfv 6489	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4564	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17222	. . . . . . 7 class le
39	2, 38	cfv 6489	. . . . . 6 class (le‘ndx)
40		cle 11175	. . . . . 6 class ≤
41	39, 40	cop 4564	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17224	. . . . . . 7 class dist
43	2, 42	cfv 6489	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4564	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4562	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17225	. . . . . . 7 class UnifSet
47	2, 46	cfv 6489	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21342	. . . . . . 7 class metUnif
49	34, 48	cfv 6489	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4564	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4558	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3883	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3883	. 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 1548	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  21353  cnfldex  21354  cnfldbas  21355  mpocnfldadd  21356  mpocnfldmul  21358  cnfldcj  21360  cnfldtset  21361  cnfldle  21362  cnfldds  21363  cnfldunif  21364  cnfldfun  21365  cnfldfunALT  21366  cffldtocusgr  29538