Definition df-cnfld 20318

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 20320, cnfldadd 20322, cnfldmul 20323, cnfldcj 20324, cnfldtset 20325, cnfldle 20326, cnfldds 20327, and cnfldbas 20321. 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 20317	. 2 class ℂfld
2		cnx 16663	. . . . . . 7 class ndx
3		cbs 16666	. . . . . . 7 class Base
4	2, 3	cfv 6358	. . . . . 6 class (Base‘ndx)
5		cc 10692	. . . . . 6 class ℂ
6	4, 5	cop 4533	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 16749	. . . . . . 7 class +g
8	2, 7	cfv 6358	. . . . . 6 class (+g‘ndx)
9		caddc 10697	. . . . . 6 class +
10	8, 9	cop 4533	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 16750	. . . . . . 7 class .r
12	2, 11	cfv 6358	. . . . . 6 class (.r‘ndx)
13		cmul 10699	. . . . . 6 class ·
14	12, 13	cop 4533	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4531	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 16751	. . . . . . 7 class *𝑟
17	2, 16	cfv 6358	. . . . . 6 class (*𝑟‘ndx)
18		ccj 14624	. . . . . 6 class ∗
19	17, 18	cop 4533	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4527	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3851	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 16755	. . . . . . 7 class TopSet
23	2, 22	cfv 6358	. . . . . 6 class (TopSet‘ndx)
24		cabs 14762	. . . . . . . 8 class abs
25		cmin 11027	. . . . . . . 8 class −
26	24, 25	ccom 5540	. . . . . . 7 class (abs ∘ − )
27		cmopn 20307	. . . . . . 7 class MetOpen
28	26, 27	cfv 6358	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4533	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 16756	. . . . . . 7 class le
31	2, 30	cfv 6358	. . . . . 6 class (le‘ndx)
32		cle 10833	. . . . . 6 class ≤
33	31, 32	cop 4533	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 16758	. . . . . . 7 class dist
35	2, 34	cfv 6358	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4533	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4531	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 16759	. . . . . . 7 class UnifSet
39	2, 38	cfv 6358	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20308	. . . . . . 7 class metUnif
41	26, 40	cfv 6358	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4533	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4527	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3851	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3851	. 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 1543	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  20319  cnfldbas  20321  cnfldadd  20322  cnfldmul  20323  cnfldcj  20324  cnfldtset  20325  cnfldle  20326  cnfldds  20327  cnfldunif  20328  cnfldfun  20329  cnfldfunALT  20330  cffldtocusgr  27489