Definition df-cnfld 14574

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 14576, cnfldadd 14579, cnfldmul 14581, cnfldcj 14582, cnfldtset 14583, cnfldle 14584, cnfldds 14585, and cnfldbas 14577. 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 14573	. 2 class ℂfld
2		cnx 13081	. . . . . . 7 class ndx
3		cbs 13084	. . . . . . 7 class Base
4	2, 3	cfv 5326	. . . . . 6 class (Base‘ndx)
5		cc 8030	. . . . . 6 class ℂ
6	4, 5	cop 3672	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13162	. . . . . . 7 class +g
8	2, 7	cfv 5326	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1396	. . . . . . . 8 class 𝑥
12	10	cv 1396	. . . . . . . 8 class 𝑦
13		caddc 8035	. . . . . . . 8 class +
14	11, 12, 13	co 6018	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6020	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3672	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13163	. . . . . . 7 class .r
18	2, 17	cfv 5326	. . . . . 6 class (.r‘ndx)
19		cmul 8037	. . . . . . . 8 class ·
20	11, 12, 19	co 6018	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6020	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3672	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3671	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13164	. . . . . . 7 class *𝑟
25	2, 24	cfv 5326	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11401	. . . . . 6 class ∗
27	25, 26	cop 3672	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3669	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3198	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13168	. . . . . . 7 class TopSet
31	2, 30	cfv 5326	. . . . . 6 class (TopSet‘ndx)
32		cabs 11559	. . . . . . . 8 class abs
33		cmin 8350	. . . . . . . 8 class −
34	32, 33	ccom 4729	. . . . . . 7 class (abs ∘ − )
35		cmopn 14558	. . . . . . 7 class MetOpen
36	34, 35	cfv 5326	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3672	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13169	. . . . . . 7 class le
39	2, 38	cfv 5326	. . . . . 6 class (le‘ndx)
40		cle 8215	. . . . . 6 class ≤
41	39, 40	cop 3672	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13171	. . . . . . 7 class dist
43	2, 42	cfv 5326	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3672	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3671	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13172	. . . . . . 7 class UnifSet
47	2, 46	cfv 5326	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14559	. . . . . . 7 class metUnif
49	34, 48	cfv 5326	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3672	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3669	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3198	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3198	. 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 1397	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  14575  cnfldbas  14577  mpocnfldadd  14578  mpocnfldmul  14580  cnfldcj  14582  cnfldtset  14583  cnfldle  14584  cnfldds  14585