Definition df-cnfld 14056

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 14058, cnfldadd 14061, cnfldmul 14063, cnfldcj 14064, cnfldtset 14065, cnfldle 14066, cnfldds 14067, and cnfldbas 14059. 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 14055	. 2 class ℂfld
2		cnx 12618	. . . . . . 7 class ndx
3		cbs 12621	. . . . . . 7 class Base
4	2, 3	cfv 5255	. . . . . 6 class (Base‘ndx)
5		cc 7872	. . . . . 6 class ℂ
6	4, 5	cop 3622	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12698	. . . . . . 7 class +g
8	2, 7	cfv 5255	. . . . . 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 7877	. . . . . . . 8 class +
14	11, 12, 13	co 5919	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 5921	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3622	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 12699	. . . . . . 7 class .r
18	2, 17	cfv 5255	. . . . . 6 class (.r‘ndx)
19		cmul 7879	. . . . . . . 8 class ·
20	11, 12, 19	co 5919	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 5921	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3622	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3621	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 12700	. . . . . . 7 class *𝑟
25	2, 24	cfv 5255	. . . . . 6 class (*𝑟‘ndx)
26		ccj 10986	. . . . . 6 class ∗
27	25, 26	cop 3622	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3619	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3152	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 12704	. . . . . . 7 class TopSet
31	2, 30	cfv 5255	. . . . . 6 class (TopSet‘ndx)
32		cabs 11144	. . . . . . . 8 class abs
33		cmin 8192	. . . . . . . 8 class −
34	32, 33	ccom 4664	. . . . . . 7 class (abs ∘ − )
35		cmopn 14040	. . . . . . 7 class MetOpen
36	34, 35	cfv 5255	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3622	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 12705	. . . . . . 7 class le
39	2, 38	cfv 5255	. . . . . 6 class (le‘ndx)
40		cle 8057	. . . . . 6 class ≤
41	39, 40	cop 3622	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 12707	. . . . . . 7 class dist
43	2, 42	cfv 5255	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3622	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3621	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 12708	. . . . . . 7 class UnifSet
47	2, 46	cfv 5255	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14041	. . . . . . 7 class metUnif
49	34, 48	cfv 5255	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3622	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3619	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3152	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3152	. 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  14057  cnfldbas  14059  mpocnfldadd  14060  mpocnfldmul  14062  cnfldcj  14064  cnfldtset  14065  cnfldle  14066  cnfldds  14067