Definition df-cnfld 20228

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ↾_s restriction operator, for instance (ℂ_fld ↾ 𝔸) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex 20230, cnfldadd 20232, cnfldmul 20233, cnfldcj 20234, cnfldtset 20235, cnfldle 20236, cnfldds 20237, and cnfldbas 20231. 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.) (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 ∘ − ))⟩}))

Detailed syntax breakdown of Definition df-cnfld

Step	Hyp	Ref	Expression
1		ccnfld 20227	. 2 class ℂfld
2		cnx 16309	. . . . . . 7 class ndx
3		cbs 16312	. . . . . . 7 class Base
4	2, 3	cfv 6225	. . . . . 6 class (Base‘ndx)
5		cc 10381	. . . . . 6 class ℂ
6	4, 5	cop 4478	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 16394	. . . . . . 7 class +g
8	2, 7	cfv 6225	. . . . . 6 class (+g‘ndx)
9		caddc 10386	. . . . . 6 class +
10	8, 9	cop 4478	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 16395	. . . . . . 7 class .r
12	2, 11	cfv 6225	. . . . . 6 class (.r‘ndx)
13		cmul 10388	. . . . . 6 class ·
14	12, 13	cop 4478	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4476	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 16396	. . . . . . 7 class *𝑟
17	2, 16	cfv 6225	. . . . . 6 class (*𝑟‘ndx)
18		ccj 14289	. . . . . 6 class ∗
19	17, 18	cop 4478	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4472	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3857	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 16400	. . . . . . 7 class TopSet
23	2, 22	cfv 6225	. . . . . 6 class (TopSet‘ndx)
24		cabs 14427	. . . . . . . 8 class abs
25		cmin 10717	. . . . . . . 8 class −
26	24, 25	ccom 5447	. . . . . . 7 class (abs ∘ − )
27		cmopn 20217	. . . . . . 7 class MetOpen
28	26, 27	cfv 6225	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4478	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 16401	. . . . . . 7 class le
31	2, 30	cfv 6225	. . . . . 6 class (le‘ndx)
32		cle 10522	. . . . . 6 class ≤
33	31, 32	cop 4478	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 16403	. . . . . . 7 class dist
35	2, 34	cfv 6225	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4478	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4476	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 16404	. . . . . . 7 class UnifSet
39	2, 38	cfv 6225	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20218	. . . . . . 7 class metUnif
41	26, 40	cfv 6225	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4478	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4472	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3857	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3857	. 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
46	1, 45	wceq 1522	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  20229  cnfldbas  20231  cnfldadd  20232  cnfldmul  20233  cnfldcj  20234  cnfldtset  20235  cnfldle  20236  cnfldds  20237  cnfldunif  20238  cnfldfun  20239  cnfldfunALT  20240  cffldtocusgr  26912