Definition df-cnfld 20607

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 20609, cnfldadd 20611, cnfldmul 20612, cnfldcj 20613, cnfldtset 20614, cnfldle 20615, cnfldds 20616, and cnfldbas 20610. 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 20606	. 2 class ℂfld
2		cnx 16903	. . . . . . 7 class ndx
3		cbs 16921	. . . . . . 7 class Base
4	2, 3	cfv 6437	. . . . . 6 class (Base‘ndx)
5		cc 10878	. . . . . 6 class ℂ
6	4, 5	cop 4568	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 16971	. . . . . . 7 class +g
8	2, 7	cfv 6437	. . . . . 6 class (+g‘ndx)
9		caddc 10883	. . . . . 6 class +
10	8, 9	cop 4568	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 16972	. . . . . . 7 class .r
12	2, 11	cfv 6437	. . . . . 6 class (.r‘ndx)
13		cmul 10885	. . . . . 6 class ·
14	12, 13	cop 4568	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4566	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 16973	. . . . . . 7 class *𝑟
17	2, 16	cfv 6437	. . . . . 6 class (*𝑟‘ndx)
18		ccj 14816	. . . . . 6 class ∗
19	17, 18	cop 4568	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4562	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3886	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 16977	. . . . . . 7 class TopSet
23	2, 22	cfv 6437	. . . . . 6 class (TopSet‘ndx)
24		cabs 14954	. . . . . . . 8 class abs
25		cmin 11214	. . . . . . . 8 class −
26	24, 25	ccom 5594	. . . . . . 7 class (abs ∘ − )
27		cmopn 20596	. . . . . . 7 class MetOpen
28	26, 27	cfv 6437	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4568	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 16978	. . . . . . 7 class le
31	2, 30	cfv 6437	. . . . . 6 class (le‘ndx)
32		cle 11019	. . . . . 6 class ≤
33	31, 32	cop 4568	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 16980	. . . . . . 7 class dist
35	2, 34	cfv 6437	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4568	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4566	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 16981	. . . . . . 7 class UnifSet
39	2, 38	cfv 6437	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20597	. . . . . . 7 class metUnif
41	26, 40	cfv 6437	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4568	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4562	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3886	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3886	. 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  20608  cnfldbas  20610  cnfldadd  20611  cnfldmul  20612  cnfldcj  20613  cnfldtset  20614  cnfldle  20615  cnfldds  20616  cnfldunif  20617  cnfldfun  20618  cnfldfunALT  20619  cnfldfunALTOLD  20620  cffldtocusgr  27823