Definition df-cnfld 20938

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 20940, cnfldadd 20942, cnfldmul 20943, cnfldcj 20944, cnfldtset 20945, cnfldle 20946, cnfldds 20947, and cnfldbas 20941. 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 20937	. 2 class ℂfld
2		cnx 17123	. . . . . . 7 class ndx
3		cbs 17141	. . . . . . 7 class Base
4	2, 3	cfv 6541	. . . . . 6 class (Base‘ndx)
5		cc 11105	. . . . . 6 class ℂ
6	4, 5	cop 4634	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17194	. . . . . . 7 class +g
8	2, 7	cfv 6541	. . . . . 6 class (+g‘ndx)
9		caddc 11110	. . . . . 6 class +
10	8, 9	cop 4634	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 17195	. . . . . . 7 class .r
12	2, 11	cfv 6541	. . . . . 6 class (.r‘ndx)
13		cmul 11112	. . . . . 6 class ·
14	12, 13	cop 4634	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4632	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 17196	. . . . . . 7 class *𝑟
17	2, 16	cfv 6541	. . . . . 6 class (*𝑟‘ndx)
18		ccj 15040	. . . . . 6 class ∗
19	17, 18	cop 4634	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4628	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3946	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 17200	. . . . . . 7 class TopSet
23	2, 22	cfv 6541	. . . . . 6 class (TopSet‘ndx)
24		cabs 15178	. . . . . . . 8 class abs
25		cmin 11441	. . . . . . . 8 class −
26	24, 25	ccom 5680	. . . . . . 7 class (abs ∘ − )
27		cmopn 20927	. . . . . . 7 class MetOpen
28	26, 27	cfv 6541	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4634	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 17201	. . . . . . 7 class le
31	2, 30	cfv 6541	. . . . . 6 class (le‘ndx)
32		cle 11246	. . . . . 6 class ≤
33	31, 32	cop 4634	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 17203	. . . . . . 7 class dist
35	2, 34	cfv 6541	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4634	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4632	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 17204	. . . . . . 7 class UnifSet
39	2, 38	cfv 6541	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20928	. . . . . . 7 class metUnif
41	26, 40	cfv 6541	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4634	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4628	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3946	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3946	. 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 1542	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  20939  cnfldbas  20941  cnfldadd  20942  cnfldmul  20943  cnfldcj  20944  cnfldtset  20945  cnfldle  20946  cnfldds  20947  cnfldunif  20948  cnfldfun  20949  cnfldfunALT  20950  cnfldfunALTOLD  20951  cffldtocusgr  28694  gg-cnfldex  35169