Definition df-cnfld 14636

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 14638, cnfldadd 14641, cnfldmul 14643, cnfldcj 14644, cnfldtset 14645, cnfldle 14646, cnfldds 14647, and cnfldbas 14639. 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 14635	. 2 class ℂfld
2		cnx 13142	. . . . . . 7 class ndx
3		cbs 13145	. . . . . . 7 class Base
4	2, 3	cfv 5333	. . . . . 6 class (Base‘ndx)
5		cc 8073	. . . . . 6 class ℂ
6	4, 5	cop 3676	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13223	. . . . . . 7 class +g
8	2, 7	cfv 5333	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1397	. . . . . . . 8 class 𝑥
12	10	cv 1397	. . . . . . . 8 class 𝑦
13		caddc 8078	. . . . . . . 8 class +
14	11, 12, 13	co 6028	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6030	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3676	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13224	. . . . . . 7 class .r
18	2, 17	cfv 5333	. . . . . 6 class (.r‘ndx)
19		cmul 8080	. . . . . . . 8 class ·
20	11, 12, 19	co 6028	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6030	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3676	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3675	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13225	. . . . . . 7 class *𝑟
25	2, 24	cfv 5333	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11462	. . . . . 6 class ∗
27	25, 26	cop 3676	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3673	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3199	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13229	. . . . . . 7 class TopSet
31	2, 30	cfv 5333	. . . . . 6 class (TopSet‘ndx)
32		cabs 11620	. . . . . . . 8 class abs
33		cmin 8393	. . . . . . . 8 class −
34	32, 33	ccom 4735	. . . . . . 7 class (abs ∘ − )
35		cmopn 14620	. . . . . . 7 class MetOpen
36	34, 35	cfv 5333	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3676	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13230	. . . . . . 7 class le
39	2, 38	cfv 5333	. . . . . 6 class (le‘ndx)
40		cle 8258	. . . . . 6 class ≤
41	39, 40	cop 3676	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13232	. . . . . . 7 class dist
43	2, 42	cfv 5333	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3676	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3675	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13233	. . . . . . 7 class UnifSet
47	2, 46	cfv 5333	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14621	. . . . . . 7 class metUnif
49	34, 48	cfv 5333	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3676	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3673	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3199	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3199	. 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 1398	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  14637  cnfldbas  14639  mpocnfldadd  14640  mpocnfldmul  14642  cnfldcj  14644  cnfldtset  14645  cnfldle  14646  cnfldds  14647