Definition df-cnfld 21365

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 21367, cnfldadd 21370, cnfldmul 21372, cnfldcj 21373, cnfldtset 21374, cnfldle 21375, cnfldds 21376, and cnfldbas 21368. 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 21364	. 2 class ℂfld
2		cnx 17230	. . . . . . 7 class ndx
3		cbs 17247	. . . . . . 7 class Base
4	2, 3	cfv 6561	. . . . . 6 class (Base‘ndx)
5		cc 11153	. . . . . 6 class ℂ
6	4, 5	cop 4632	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17297	. . . . . . 7 class +g
8	2, 7	cfv 6561	. . . . . 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 11158	. . . . . . . 8 class +
14	11, 12, 13	co 7431	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7433	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4632	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17298	. . . . . . 7 class .r
18	2, 17	cfv 6561	. . . . . 6 class (.r‘ndx)
19		cmul 11160	. . . . . . . 8 class ·
20	11, 12, 19	co 7431	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7433	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4632	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4630	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17299	. . . . . . 7 class *𝑟
25	2, 24	cfv 6561	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15135	. . . . . 6 class ∗
27	25, 26	cop 4632	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4626	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3949	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17303	. . . . . . 7 class TopSet
31	2, 30	cfv 6561	. . . . . 6 class (TopSet‘ndx)
32		cabs 15273	. . . . . . . 8 class abs
33		cmin 11492	. . . . . . . 8 class −
34	32, 33	ccom 5689	. . . . . . 7 class (abs ∘ − )
35		cmopn 21354	. . . . . . 7 class MetOpen
36	34, 35	cfv 6561	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4632	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17304	. . . . . . 7 class le
39	2, 38	cfv 6561	. . . . . 6 class (le‘ndx)
40		cle 11296	. . . . . 6 class ≤
41	39, 40	cop 4632	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17306	. . . . . . 7 class dist
43	2, 42	cfv 6561	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4632	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4630	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17307	. . . . . . 7 class UnifSet
47	2, 46	cfv 6561	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21355	. . . . . . 7 class metUnif
49	34, 48	cfv 6561	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4632	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4626	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3949	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3949	. 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  21366  cnfldex  21367  cnfldbas  21368  mpocnfldadd  21369  mpocnfldmul  21371  cnfldcj  21373  cnfldtset  21374  cnfldle  21375  cnfldds  21376  cnfldunif  21377  cnfldfun  21378  cnfldfunALT  21379  dfcnfldOLD  21380  cffldtocusgr  29464