Definition df-cnfld 15004

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 15006, cnfldadd 15009, cnfldmul 15011, cnfldcj 15012, cnfldtset 15013, cnfldle 15014, cnfldds 15015, and cnfldbas 15007. 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 15003	. 2 class ℂfld
2		cnx 13408	. . . . . . 7 class ndx
3		cbs 13411	. . . . . . 7 class Base
4	2, 3	cfv 5380	. . . . . 6 class (Base‘ndx)
5		cc 8184	. . . . . 6 class ℂ
6	4, 5	cop 3712	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 13491	. . . . . . 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 8189	. . . . . . . 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 13492	. . . . . . 7 class .r
18	2, 17	cfv 5380	. . . . . 6 class (.r‘ndx)
19		cmul 8191	. . . . . . . 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 13493	. . . . . . 7 class *𝑟
25	2, 24	cfv 5380	. . . . . 6 class (*𝑟‘ndx)
26		ccj 11627	. . . . . 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 13497	. . . . . . 7 class TopSet
31	2, 30	cfv 5380	. . . . . 6 class (TopSet‘ndx)
32		cabs 11786	. . . . . . . 8 class abs
33		cmin 8505	. . . . . . . 8 class −
34	32, 33	ccom 4780	. . . . . . 7 class (abs ∘ − )
35		cmopn 14988	. . . . . . 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 13498	. . . . . . 7 class le
39	2, 38	cfv 5380	. . . . . 6 class (le‘ndx)
40		cle 8368	. . . . . 6 class ≤
41	39, 40	cop 3712	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 13500	. . . . . . 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 13501	. . . . . . 7 class UnifSet
47	2, 46	cfv 5380	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 14989	. . . . . . 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  15005  cnfldbas  15007  mpocnfldadd  15008  mpocnfldmul  15010  cnfldcj  15012  cnfldtset  15013  cnfldle  15014  cnfldds  15015