Definition df-cnfld 14564

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 14566, cnfldadd 14569, cnfldmul 14571, cnfldcj 14572, cnfldtset 14573, cnfldle 14574, cnfldds 14575, and cnfldbas 14567. 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 14563	. 2 class ℂfld
2		cnx 13072	. . . . . . 7 class ndx
3		cbs 13075	. . . . . . 7 class Base
4	2, 3	cfv 5324	. . . . . 6 class (Base‘ndx)
5		cc 8023	. . . . . 6 class ℂ
6	4, 5	cop 3670	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13153	. . . . . . 7 class +g
8	2, 7	cfv 5324	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1394	. . . . . . . 8 class 𝑥
12	10	cv 1394	. . . . . . . 8 class 𝑦
13		caddc 8028	. . . . . . . 8 class +
14	11, 12, 13	co 6013	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6015	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3670	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13154	. . . . . . 7 class .r
18	2, 17	cfv 5324	. . . . . 6 class (.r‘ndx)
19		cmul 8030	. . . . . . . 8 class ·
20	11, 12, 19	co 6013	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6015	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3670	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3669	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13155	. . . . . . 7 class *𝑟
25	2, 24	cfv 5324	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11393	. . . . . 6 class ∗
27	25, 26	cop 3670	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3667	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3196	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13159	. . . . . . 7 class TopSet
31	2, 30	cfv 5324	. . . . . 6 class (TopSet‘ndx)
32		cabs 11551	. . . . . . . 8 class abs
33		cmin 8343	. . . . . . . 8 class −
34	32, 33	ccom 4727	. . . . . . 7 class (abs ∘ − )
35		cmopn 14548	. . . . . . 7 class MetOpen
36	34, 35	cfv 5324	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3670	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13160	. . . . . . 7 class le
39	2, 38	cfv 5324	. . . . . 6 class (le‘ndx)
40		cle 8208	. . . . . 6 class ≤
41	39, 40	cop 3670	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13162	. . . . . . 7 class dist
43	2, 42	cfv 5324	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3670	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3669	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13163	. . . . . . 7 class UnifSet
47	2, 46	cfv 5324	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14549	. . . . . . 7 class metUnif
49	34, 48	cfv 5324	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3670	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3667	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3196	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3196	. 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 1395	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  14565  cnfldbas  14567  mpocnfldadd  14568  mpocnfldmul  14570  cnfldcj  14572  cnfldtset  14573  cnfldle  14574  cnfldds  14575