Definition df-cnfld 14943

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 14945, cnfldadd 14948, cnfldmul 14950, cnfldcj 14951, cnfldtset 14952, cnfldle 14953, cnfldds 14954, and cnfldbas 14946. 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 14942	. 2 class ℂfld
2		cnx 13398	. . . . . . 7 class ndx
3		cbs 13401	. . . . . . 7 class Base
4	2, 3	cfv 5377	. . . . . 6 class (Base‘ndx)
5		cc 8177	. . . . . 6 class ℂ
6	4, 5	cop 3712	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13480	. . . . . . 7 class +g
8	2, 7	cfv 5377	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1401	. . . . . . . 8 class 𝑥
12	10	cv 1401	. . . . . . . 8 class 𝑦
13		caddc 8182	. . . . . . . 8 class +
14	11, 12, 13	co 6085	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6087	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3712	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13481	. . . . . . 7 class .r
18	2, 17	cfv 5377	. . . . . 6 class (.r‘ndx)
19		cmul 8184	. . . . . . . 8 class ·
20	11, 12, 19	co 6085	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6087	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3712	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3711	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13482	. . . . . . 7 class *𝑟
25	2, 24	cfv 5377	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11618	. . . . . 6 class ∗
27	25, 26	cop 3712	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3709	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3218	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13486	. . . . . . 7 class TopSet
31	2, 30	cfv 5377	. . . . . 6 class (TopSet‘ndx)
32		cabs 11777	. . . . . . . 8 class abs
33		cmin 8498	. . . . . . . 8 class −
34	32, 33	ccom 4778	. . . . . . 7 class (abs ∘ − )
35		cmopn 14927	. . . . . . 7 class MetOpen
36	34, 35	cfv 5377	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3712	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13487	. . . . . . 7 class le
39	2, 38	cfv 5377	. . . . . 6 class (le‘ndx)
40		cle 8361	. . . . . 6 class ≤
41	39, 40	cop 3712	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13489	. . . . . . 7 class dist
43	2, 42	cfv 5377	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3712	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3711	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13490	. . . . . . 7 class UnifSet
47	2, 46	cfv 5377	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14928	. . . . . . 7 class metUnif
49	34, 48	cfv 5377	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3712	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3709	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3218	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3218	. 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 1402	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  14944  cnfldbas  14946  mpocnfldadd  14947  mpocnfldmul  14949  cnfldcj  14951  cnfldtset  14952  cnfldle  14953  cnfldds  14954