Definition df-cnfld 15002

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 15004, cnfldadd 15007, cnfldmul 15009, cnfldcj 15010, cnfldtset 15011, cnfldle 15012, cnfldds 15013, and cnfldbas 15005. 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 15001	. 2 class ℂfld
2		cnx 13406	. . . . . . 7 class ndx
3		cbs 13409	. . . . . . 7 class Base
4	2, 3	cfv 5380	. . . . . 6 class (Base‘ndx)
5		cc 8183	. . . . . 6 class ℂ
6	4, 5	cop 3712	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13489	. . . . . . 7 class +g
8	2, 7	cfv 5380	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1401	. . . . . . . 8 class 𝑥
12	10	cv 1401	. . . . . . . 8 class 𝑦
13		caddc 8188	. . . . . . . 8 class +
14	11, 12, 13	co 6088	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 6090	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 3712	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 13490	. . . . . . 7 class .r
18	2, 17	cfv 5380	. . . . . 6 class (.r‘ndx)
19		cmul 8190	. . . . . . . 8 class ·
20	11, 12, 19	co 6088	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 6090	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 3712	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 3711	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 13491	. . . . . . 7 class *𝑟
25	2, 24	cfv 5380	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11625	. . . . . 6 class ∗
27	25, 26	cop 3712	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 3709	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3218	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 13495	. . . . . . 7 class TopSet
31	2, 30	cfv 5380	. . . . . 6 class (TopSet‘ndx)
32		cabs 11784	. . . . . . . 8 class abs
33		cmin 8504	. . . . . . . 8 class −
34	32, 33	ccom 4780	. . . . . . 7 class (abs ∘ − )
35		cmopn 14986	. . . . . . 7 class MetOpen
36	34, 35	cfv 5380	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 3712	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 13496	. . . . . . 7 class le
39	2, 38	cfv 5380	. . . . . 6 class (le‘ndx)
40		cle 8367	. . . . . 6 class ≤
41	39, 40	cop 3712	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13498	. . . . . . 7 class dist
43	2, 42	cfv 5380	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 3712	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 3711	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 13499	. . . . . . 7 class UnifSet
47	2, 46	cfv 5380	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14987	. . . . . . 7 class metUnif
49	34, 48	cfv 5380	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 3712	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 3709	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3218	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3218	. 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 1402	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 used by:  cnfldstr  15003  cnfldbas  15005  mpocnfldadd  15006  mpocnfldmul  15008  cnfldcj  15010  cnfldtset  15011  cnfldle  15012  cnfldds  15013