Definition df-cnfld 21145

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 21147, cnfldadd 21149, cnfldmul 21150, cnfldcj 21151, cnfldtset 21152, cnfldle 21153, cnfldds 21154, and cnfldbas 21148. 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 21144	. 2 class ℂfld
2		cnx 17130	. . . . . . 7 class ndx
3		cbs 17148	. . . . . . 7 class Base
4	2, 3	cfv 6542	. . . . . 6 class (Base‘ndx)
5		cc 11110	. . . . . 6 class ℂ
6	4, 5	cop 4633	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17201	. . . . . . 7 class +g
8	2, 7	cfv 6542	. . . . . 6 class (+g‘ndx)
9		caddc 11115	. . . . . 6 class +
10	8, 9	cop 4633	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 17202	. . . . . . 7 class .r
12	2, 11	cfv 6542	. . . . . 6 class (.r‘ndx)
13		cmul 11117	. . . . . 6 class ·
14	12, 13	cop 4633	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4631	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 17203	. . . . . . 7 class *𝑟
17	2, 16	cfv 6542	. . . . . 6 class (*𝑟‘ndx)
18		ccj 15047	. . . . . 6 class ∗
19	17, 18	cop 4633	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4627	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3945	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 17207	. . . . . . 7 class TopSet
23	2, 22	cfv 6542	. . . . . 6 class (TopSet‘ndx)
24		cabs 15185	. . . . . . . 8 class abs
25		cmin 11448	. . . . . . . 8 class −
26	24, 25	ccom 5679	. . . . . . 7 class (abs ∘ − )
27		cmopn 21134	. . . . . . 7 class MetOpen
28	26, 27	cfv 6542	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4633	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 17208	. . . . . . 7 class le
31	2, 30	cfv 6542	. . . . . 6 class (le‘ndx)
32		cle 11253	. . . . . 6 class ≤
33	31, 32	cop 4633	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 17210	. . . . . . 7 class dist
35	2, 34	cfv 6542	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4633	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4631	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 17211	. . . . . . 7 class UnifSet
39	2, 38	cfv 6542	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 21135	. . . . . . 7 class metUnif
41	26, 40	cfv 6542	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4633	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4627	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3945	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3945	. 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  21146  cnfldbas  21148  cnfldadd  21149  cnfldmul  21150  cnfldcj  21151  cnfldtset  21152  cnfldle  21153  cnfldds  21154  cnfldunif  21155  cnfldfun  21156  cnfldfunALT  21157  cnfldfunALTOLD  21158  cffldtocusgr  28971  gg-cnfldex  35467  gg-dfcnfld  35473