Definition df-cnfld 20546

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 20548, cnfldadd 20550, cnfldmul 20551, cnfldcj 20552, cnfldtset 20553, cnfldle 20554, cnfldds 20555, and cnfldbas 20549. 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 20545	. 2 class ℂfld
2		cnx 16480	. . . . . . 7 class ndx
3		cbs 16483	. . . . . . 7 class Base
4	2, 3	cfv 6355	. . . . . 6 class (Base‘ndx)
5		cc 10535	. . . . . 6 class ℂ
6	4, 5	cop 4573	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 16565	. . . . . . 7 class +g
8	2, 7	cfv 6355	. . . . . 6 class (+g‘ndx)
9		caddc 10540	. . . . . 6 class +
10	8, 9	cop 4573	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 16566	. . . . . . 7 class .r
12	2, 11	cfv 6355	. . . . . 6 class (.r‘ndx)
13		cmul 10542	. . . . . 6 class ·
14	12, 13	cop 4573	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4571	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 16567	. . . . . . 7 class *𝑟
17	2, 16	cfv 6355	. . . . . 6 class (*𝑟‘ndx)
18		ccj 14455	. . . . . 6 class ∗
19	17, 18	cop 4573	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4567	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3934	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 16571	. . . . . . 7 class TopSet
23	2, 22	cfv 6355	. . . . . 6 class (TopSet‘ndx)
24		cabs 14593	. . . . . . . 8 class abs
25		cmin 10870	. . . . . . . 8 class −
26	24, 25	ccom 5559	. . . . . . 7 class (abs ∘ − )
27		cmopn 20535	. . . . . . 7 class MetOpen
28	26, 27	cfv 6355	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4573	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 16572	. . . . . . 7 class le
31	2, 30	cfv 6355	. . . . . 6 class (le‘ndx)
32		cle 10676	. . . . . 6 class ≤
33	31, 32	cop 4573	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 16574	. . . . . . 7 class dist
35	2, 34	cfv 6355	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4573	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4571	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 16575	. . . . . . 7 class UnifSet
39	2, 38	cfv 6355	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20536	. . . . . . 7 class metUnif
41	26, 40	cfv 6355	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4573	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4567	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3934	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3934	. 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 1537	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  20547  cnfldbas  20549  cnfldadd  20550  cnfldmul  20551  cnfldcj  20552  cnfldtset  20553  cnfldle  20554  cnfldds  20555  cnfldunif  20556  cnfldfun  20557  cnfldfunALT  20558  cffldtocusgr  27229