Definition df-cnfld 21272

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 21274, cnfldadd 21277, cnfldmul 21279, cnfldcj 21280, cnfldtset 21281, cnfldle 21282, cnfldds 21283, and cnfldbas 21275. 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 21271	. 2 class ℂfld
2		cnx 17170	. . . . . . 7 class ndx
3		cbs 17186	. . . . . . 7 class Base
4	2, 3	cfv 6514	. . . . . 6 class (Base‘ndx)
5		cc 11073	. . . . . 6 class ℂ
6	4, 5	cop 4598	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17227	. . . . . . 7 class +g
8	2, 7	cfv 6514	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1539	. . . . . . . 8 class 𝑥
12	10	cv 1539	. . . . . . . 8 class 𝑦
13		caddc 11078	. . . . . . . 8 class +
14	11, 12, 13	co 7390	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7392	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4598	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17228	. . . . . . 7 class .r
18	2, 17	cfv 6514	. . . . . 6 class (.r‘ndx)
19		cmul 11080	. . . . . . . 8 class ·
20	11, 12, 19	co 7390	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7392	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4598	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4596	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17229	. . . . . . 7 class *𝑟
25	2, 24	cfv 6514	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15069	. . . . . 6 class ∗
27	25, 26	cop 4598	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4592	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3915	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17233	. . . . . . 7 class TopSet
31	2, 30	cfv 6514	. . . . . 6 class (TopSet‘ndx)
32		cabs 15207	. . . . . . . 8 class abs
33		cmin 11412	. . . . . . . 8 class −
34	32, 33	ccom 5645	. . . . . . 7 class (abs ∘ − )
35		cmopn 21261	. . . . . . 7 class MetOpen
36	34, 35	cfv 6514	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4598	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17234	. . . . . . 7 class le
39	2, 38	cfv 6514	. . . . . 6 class (le‘ndx)
40		cle 11216	. . . . . 6 class ≤
41	39, 40	cop 4598	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17236	. . . . . . 7 class dist
43	2, 42	cfv 6514	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4598	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4596	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17237	. . . . . . 7 class UnifSet
47	2, 46	cfv 6514	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21262	. . . . . . 7 class metUnif
49	34, 48	cfv 6514	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4598	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4592	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3915	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3915	. 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 1540	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  21273  cnfldex  21274  cnfldbas  21275  mpocnfldadd  21276  mpocnfldmul  21278  cnfldcj  21280  cnfldtset  21281  cnfldle  21282  cnfldds  21283  cnfldunif  21284  cnfldfun  21285  cnfldfunALT  21286  dfcnfldOLD  21287  cffldtocusgr  29381