Definition df-cnfld 14363

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 14365, cnfldadd 14368, cnfldmul 14370, cnfldcj 14371, cnfldtset 14372, cnfldle 14373, cnfldds 14374, and cnfldbas 14366. 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 14362	. 2 class ℂfld
2		cnx 12873	. . . . . . 7 class ndx
3		cbs 12876	. . . . . . 7 class Base
4	2, 3	cfv 5276	. . . . . 6 class (Base‘ndx)
5		cc 7930	. . . . . 6 class ℂ
6	4, 5	cop 3637	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12953	. . . . . . 7 class +g
8	2, 7	cfv 5276	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1372	. . . . . . . 8 class 𝑥
12	10	cv 1372	. . . . . . . 8 class 𝑦
13		caddc 7935	. . . . . . . 8 class +
14	11, 12, 13	co 5951	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 5953	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3637	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 12954	. . . . . . 7 class .r
18	2, 17	cfv 5276	. . . . . 6 class (.r‘ndx)
19		cmul 7937	. . . . . . . 8 class ·
20	11, 12, 19	co 5951	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 5953	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3637	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3636	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 12955	. . . . . . 7 class *𝑟
25	2, 24	cfv 5276	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11194	. . . . . 6 class ∗
27	25, 26	cop 3637	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3634	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3165	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 12959	. . . . . . 7 class TopSet
31	2, 30	cfv 5276	. . . . . 6 class (TopSet‘ndx)
32		cabs 11352	. . . . . . . 8 class abs
33		cmin 8250	. . . . . . . 8 class −
34	32, 33	ccom 4683	. . . . . . 7 class (abs ∘ − )
35		cmopn 14347	. . . . . . 7 class MetOpen
36	34, 35	cfv 5276	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3637	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 12960	. . . . . . 7 class le
39	2, 38	cfv 5276	. . . . . 6 class (le‘ndx)
40		cle 8115	. . . . . 6 class ≤
41	39, 40	cop 3637	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 12962	. . . . . . 7 class dist
43	2, 42	cfv 5276	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3637	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3636	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 12963	. . . . . . 7 class UnifSet
47	2, 46	cfv 5276	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14348	. . . . . . 7 class metUnif
49	34, 48	cfv 5276	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3637	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3634	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3165	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3165	. 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 1373	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  14364  cnfldbas  14366  mpocnfldadd  14367  mpocnfldmul  14369  cnfldcj  14371  cnfldtset  14372  cnfldle  14373  cnfldds  14374