Definition df-cnfld 20511

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 20513, cnfldadd 20515, cnfldmul 20516, cnfldcj 20517, cnfldtset 20518, cnfldle 20519, cnfldds 20520, and cnfldbas 20514. 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 20510	. 2 class ℂfld
2		cnx 16822	. . . . . . 7 class ndx
3		cbs 16840	. . . . . . 7 class Base
4	2, 3	cfv 6418	. . . . . 6 class (Base‘ndx)
5		cc 10800	. . . . . 6 class ℂ
6	4, 5	cop 4564	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 16888	. . . . . . 7 class +g
8	2, 7	cfv 6418	. . . . . 6 class (+g‘ndx)
9		caddc 10805	. . . . . 6 class +
10	8, 9	cop 4564	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 16889	. . . . . . 7 class .r
12	2, 11	cfv 6418	. . . . . 6 class (.r‘ndx)
13		cmul 10807	. . . . . 6 class ·
14	12, 13	cop 4564	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4562	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 16890	. . . . . . 7 class *𝑟
17	2, 16	cfv 6418	. . . . . 6 class (*𝑟‘ndx)
18		ccj 14735	. . . . . 6 class ∗
19	17, 18	cop 4564	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4558	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3881	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 16894	. . . . . . 7 class TopSet
23	2, 22	cfv 6418	. . . . . 6 class (TopSet‘ndx)
24		cabs 14873	. . . . . . . 8 class abs
25		cmin 11135	. . . . . . . 8 class −
26	24, 25	ccom 5584	. . . . . . 7 class (abs ∘ − )
27		cmopn 20500	. . . . . . 7 class MetOpen
28	26, 27	cfv 6418	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4564	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 16895	. . . . . . 7 class le
31	2, 30	cfv 6418	. . . . . 6 class (le‘ndx)
32		cle 10941	. . . . . 6 class ≤
33	31, 32	cop 4564	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 16897	. . . . . . 7 class dist
35	2, 34	cfv 6418	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4564	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4562	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 16898	. . . . . . 7 class UnifSet
39	2, 38	cfv 6418	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20501	. . . . . . 7 class metUnif
41	26, 40	cfv 6418	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4564	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4558	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3881	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3881	. 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 1539	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  20512  cnfldbas  20514  cnfldadd  20515  cnfldmul  20516  cnfldcj  20517  cnfldtset  20518  cnfldle  20519  cnfldds  20520  cnfldunif  20521  cnfldfun  20522  cnfldfunALT  20523  cffldtocusgr  27717