Definition df-cnfld 21327

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 21329, cnfldadd 21332, cnfldmul 21334, cnfldcj 21335, cnfldtset 21336, cnfldle 21337, cnfldds 21338, and cnfldbas 21330. 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 21326	. 2 class ℂfld
2		cnx 17134	. . . . . . 7 class ndx
3		cbs 17150	. . . . . . 7 class Base
4	2, 3	cfv 6502	. . . . . 6 class (Base‘ndx)
5		cc 11038	. . . . . 6 class ℂ
6	4, 5	cop 4588	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17191	. . . . . . 7 class +g
8	2, 7	cfv 6502	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1541	. . . . . . . 8 class 𝑥
12	10	cv 1541	. . . . . . . 8 class 𝑦
13		caddc 11043	. . . . . . . 8 class +
14	11, 12, 13	co 7370	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7372	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4588	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17192	. . . . . . 7 class .r
18	2, 17	cfv 6502	. . . . . 6 class (.r‘ndx)
19		cmul 11045	. . . . . . . 8 class ·
20	11, 12, 19	co 7370	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7372	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4588	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4586	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17193	. . . . . . 7 class *𝑟
25	2, 24	cfv 6502	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15033	. . . . . 6 class ∗
27	25, 26	cop 4588	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4582	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3901	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17197	. . . . . . 7 class TopSet
31	2, 30	cfv 6502	. . . . . 6 class (TopSet‘ndx)
32		cabs 15171	. . . . . . . 8 class abs
33		cmin 11378	. . . . . . . 8 class −
34	32, 33	ccom 5638	. . . . . . 7 class (abs ∘ − )
35		cmopn 21316	. . . . . . 7 class MetOpen
36	34, 35	cfv 6502	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4588	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17198	. . . . . . 7 class le
39	2, 38	cfv 6502	. . . . . 6 class (le‘ndx)
40		cle 11181	. . . . . 6 class ≤
41	39, 40	cop 4588	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17200	. . . . . . 7 class dist
43	2, 42	cfv 6502	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4588	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4586	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17201	. . . . . . 7 class UnifSet
47	2, 46	cfv 6502	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21317	. . . . . . 7 class metUnif
49	34, 48	cfv 6502	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4588	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4582	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3901	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3901	. 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 1542	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  21328  cnfldex  21329  cnfldbas  21330  mpocnfldadd  21331  mpocnfldmul  21333  cnfldcj  21335  cnfldtset  21336  cnfldle  21337  cnfldds  21338  cnfldunif  21339  cnfldfun  21340  cnfldfunALT  21341  dfcnfldOLD  21342  cffldtocusgr  29538