Definition df-cnfld 21494

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ↾_s restriction operator, for instance (ℂ_fld ↾ 𝔸) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex 21496, cnfldadd 21499, cnfldmul 21501, cnfldcj 21502, cnfldtset 21503, cnfldle 21504, cnfldds 21505, and cnfldbas 21497. 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 21493	. 2 class ℂfld
2		cnx 17255	. . . . . . 7 class ndx
3		cbs 17271	. . . . . . 7 class Base
4	2, 3	cfv 6539	. . . . . 6 class (Base‘ndx)
5		cc 11100	. . . . . 6 class ℂ
6	4, 5	cop 4600	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17312	. . . . . . 7 class +g
8	2, 7	cfv 6539	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1566	. . . . . . . 8 class 𝑥
12	10	cv 1566	. . . . . . . 8 class 𝑦
13		caddc 11105	. . . . . . . 8 class +
14	11, 12, 13	co 7413	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7415	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4600	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17313	. . . . . . 7 class .r
18	2, 17	cfv 6539	. . . . . 6 class (.r‘ndx)
19		cmul 11107	. . . . . . . 8 class ·
20	11, 12, 19	co 7413	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7415	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4600	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4598	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17314	. . . . . . 7 class *𝑟
25	2, 24	cfv 6539	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15149	. . . . . 6 class ∗
27	25, 26	cop 4600	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4594	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3911	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17318	. . . . . . 7 class TopSet
31	2, 30	cfv 6539	. . . . . 6 class (TopSet‘ndx)
32		cabs 15287	. . . . . . . 8 class abs
33		cmin 11443	. . . . . . . 8 class −
34	32, 33	ccom 5668	. . . . . . 7 class (abs ∘ − )
35		cmopn 21483	. . . . . . 7 class MetOpen
36	34, 35	cfv 6539	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4600	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17319	. . . . . . 7 class le
39	2, 38	cfv 6539	. . . . . 6 class (le‘ndx)
40		cle 11246	. . . . . 6 class ≤
41	39, 40	cop 4600	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17321	. . . . . . 7 class dist
43	2, 42	cfv 6539	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4600	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4598	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17322	. . . . . . 7 class UnifSet
47	2, 46	cfv 6539	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21484	. . . . . . 7 class metUnif
49	34, 48	cfv 6539	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4600	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4594	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3911	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3911	. 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 1567	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  21495  cnfldex  21496  cnfldbas  21497  mpocnfldadd  21498  mpocnfldmul  21500  cnfldcj  21502  cnfldtset  21503  cnfldle  21504  cnfldds  21505  cnfldunif  21506  cnfldfun  21507  cnfldfunALT  21508  cffldtocusgr  29740