Definition df-cnfld 19747

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 19749, cnfldadd 19751, cnfldmul 19752, cnfldcj 19753, cnfldtset 19754, cnfldle 19755, cnfldds 19756, and cnfldbas 19750. 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 19746	. 2 class ℂfld
2		cnx 15854	. . . . . . 7 class ndx
3		cbs 15857	. . . . . . 7 class Base
4	2, 3	cfv 5888	. . . . . 6 class (Base‘ndx)
5		cc 9934	. . . . . 6 class ℂ
6	4, 5	cop 4183	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 15941	. . . . . . 7 class +g
8	2, 7	cfv 5888	. . . . . 6 class (+g‘ndx)
9		caddc 9939	. . . . . 6 class +
10	8, 9	cop 4183	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 15942	. . . . . . 7 class .r
12	2, 11	cfv 5888	. . . . . 6 class (.r‘ndx)
13		cmul 9941	. . . . . 6 class ·
14	12, 13	cop 4183	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4181	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 15943	. . . . . . 7 class *𝑟
17	2, 16	cfv 5888	. . . . . 6 class (*𝑟‘ndx)
18		ccj 13836	. . . . . 6 class ∗
19	17, 18	cop 4183	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4177	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3572	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 15947	. . . . . . 7 class TopSet
23	2, 22	cfv 5888	. . . . . 6 class (TopSet‘ndx)
24		cabs 13974	. . . . . . . 8 class abs
25		cmin 10266	. . . . . . . 8 class −
26	24, 25	ccom 5118	. . . . . . 7 class (abs ∘ − )
27		cmopn 19736	. . . . . . 7 class MetOpen
28	26, 27	cfv 5888	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4183	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 15948	. . . . . . 7 class le
31	2, 30	cfv 5888	. . . . . 6 class (le‘ndx)
32		cle 10075	. . . . . 6 class ≤
33	31, 32	cop 4183	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 15950	. . . . . . 7 class dist
35	2, 34	cfv 5888	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4183	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4181	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 15951	. . . . . . 7 class UnifSet
39	2, 38	cfv 5888	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 19737	. . . . . . 7 class metUnif
41	26, 40	cfv 5888	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4183	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4177	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3572	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3572	. 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 1483	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  19748  cnfldbas  19750  cnfldadd  19751  cnfldmul  19752  cnfldcj  19753  cnfldtset  19754  cnfldle  19755  cnfldds  19756  cnfldunif  19757  cnfldfun  19758  cnfldfunALT  19759  cffldtocusgr  26343