Definition df-cnfld 14191

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 14193, cnfldadd 14196, cnfldmul 14198, cnfldcj 14199, cnfldtset 14200, cnfldle 14201, cnfldds 14202, and cnfldbas 14194. 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 14190	. 2 class ℂfld
2		cnx 12702	. . . . . . 7 class ndx
3		cbs 12705	. . . . . . 7 class Base
4	2, 3	cfv 5259	. . . . . 6 class (Base‘ndx)
5		cc 7896	. . . . . 6 class ℂ
6	4, 5	cop 3626	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12782	. . . . . . 7 class +g
8	2, 7	cfv 5259	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1363	. . . . . . . 8 class 𝑥
12	10	cv 1363	. . . . . . . 8 class 𝑦
13		caddc 7901	. . . . . . . 8 class +
14	11, 12, 13	co 5925	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 5927	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3626	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 12783	. . . . . . 7 class .r
18	2, 17	cfv 5259	. . . . . 6 class (.r‘ndx)
19		cmul 7903	. . . . . . . 8 class ·
20	11, 12, 19	co 5925	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 5927	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3626	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3625	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 12784	. . . . . . 7 class *𝑟
25	2, 24	cfv 5259	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11023	. . . . . 6 class ∗
27	25, 26	cop 3626	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3623	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3155	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 12788	. . . . . . 7 class TopSet
31	2, 30	cfv 5259	. . . . . 6 class (TopSet‘ndx)
32		cabs 11181	. . . . . . . 8 class abs
33		cmin 8216	. . . . . . . 8 class −
34	32, 33	ccom 4668	. . . . . . 7 class (abs ∘ − )
35		cmopn 14175	. . . . . . 7 class MetOpen
36	34, 35	cfv 5259	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3626	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 12789	. . . . . . 7 class le
39	2, 38	cfv 5259	. . . . . 6 class (le‘ndx)
40		cle 8081	. . . . . 6 class ≤
41	39, 40	cop 3626	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 12791	. . . . . . 7 class dist
43	2, 42	cfv 5259	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3626	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3625	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 12792	. . . . . . 7 class UnifSet
47	2, 46	cfv 5259	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14176	. . . . . . 7 class metUnif
49	34, 48	cfv 5259	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3626	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3623	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3155	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3155	. 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 1364	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  14192  cnfldbas  14194  mpocnfldadd  14195  mpocnfldmul  14197  cnfldcj  14199  cnfldtset  14200  cnfldle  14201  cnfldds  14202