Definition df-cnfld 14529

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 14531, cnfldadd 14534, cnfldmul 14536, cnfldcj 14537, cnfldtset 14538, cnfldle 14539, cnfldds 14540, and cnfldbas 14532. 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 14528	. 2 class ℂfld
2		cnx 13037	. . . . . . 7 class ndx
3		cbs 13040	. . . . . . 7 class Base
4	2, 3	cfv 5318	. . . . . 6 class (Base‘ndx)
5		cc 8005	. . . . . 6 class ℂ
6	4, 5	cop 3669	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13118	. . . . . . 7 class +g
8	2, 7	cfv 5318	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1394	. . . . . . . 8 class 𝑥
12	10	cv 1394	. . . . . . . 8 class 𝑦
13		caddc 8010	. . . . . . . 8 class +
14	11, 12, 13	co 6007	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6009	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3669	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13119	. . . . . . 7 class .r
18	2, 17	cfv 5318	. . . . . 6 class (.r‘ndx)
19		cmul 8012	. . . . . . . 8 class ·
20	11, 12, 19	co 6007	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6009	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3669	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3668	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13120	. . . . . . 7 class *𝑟
25	2, 24	cfv 5318	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11358	. . . . . 6 class ∗
27	25, 26	cop 3669	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3666	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3195	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13124	. . . . . . 7 class TopSet
31	2, 30	cfv 5318	. . . . . 6 class (TopSet‘ndx)
32		cabs 11516	. . . . . . . 8 class abs
33		cmin 8325	. . . . . . . 8 class −
34	32, 33	ccom 4723	. . . . . . 7 class (abs ∘ − )
35		cmopn 14513	. . . . . . 7 class MetOpen
36	34, 35	cfv 5318	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3669	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13125	. . . . . . 7 class le
39	2, 38	cfv 5318	. . . . . 6 class (le‘ndx)
40		cle 8190	. . . . . 6 class ≤
41	39, 40	cop 3669	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13127	. . . . . . 7 class dist
43	2, 42	cfv 5318	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3669	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3668	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13128	. . . . . . 7 class UnifSet
47	2, 46	cfv 5318	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14514	. . . . . . 7 class metUnif
49	34, 48	cfv 5318	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3669	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3666	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3195	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3195	. 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 1395	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  14530  cnfldbas  14532  mpocnfldadd  14533  mpocnfldmul  14535  cnfldcj  14537  cnfldtset  14538  cnfldle  14539  cnfldds  14540