Definition df-cnfld 20945

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 20947, cnfldadd 20949, cnfldmul 20950, cnfldcj 20951, cnfldtset 20952, cnfldle 20953, cnfldds 20954, and cnfldbas 20948. 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 20944	. 2 class ℂfld
2		cnx 17126	. . . . . . 7 class ndx
3		cbs 17144	. . . . . . 7 class Base
4	2, 3	cfv 6544	. . . . . 6 class (Base‘ndx)
5		cc 11108	. . . . . 6 class ℂ
6	4, 5	cop 4635	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17197	. . . . . . 7 class +g
8	2, 7	cfv 6544	. . . . . 6 class (+g‘ndx)
9		caddc 11113	. . . . . 6 class +
10	8, 9	cop 4635	. . . . 5 class ⟨(+g‘ndx), + ⟩
11		cmulr 17198	. . . . . . 7 class .r
12	2, 11	cfv 6544	. . . . . 6 class (.r‘ndx)
13		cmul 11115	. . . . . 6 class ·
14	12, 13	cop 4635	. . . . 5 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 4633	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 17199	. . . . . . 7 class *𝑟
17	2, 16	cfv 6544	. . . . . 6 class (*𝑟‘ndx)
18		ccj 15043	. . . . . 6 class ∗
19	17, 18	cop 4635	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 4629	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3947	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22		cts 17203	. . . . . . 7 class TopSet
23	2, 22	cfv 6544	. . . . . 6 class (TopSet‘ndx)
24		cabs 15181	. . . . . . . 8 class abs
25		cmin 11444	. . . . . . . 8 class −
26	24, 25	ccom 5681	. . . . . . 7 class (abs ∘ − )
27		cmopn 20934	. . . . . . 7 class MetOpen
28	26, 27	cfv 6544	. . . . . 6 class (MetOpen‘(abs ∘ − ))
29	23, 28	cop 4635	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
30		cple 17204	. . . . . . 7 class le
31	2, 30	cfv 6544	. . . . . 6 class (le‘ndx)
32		cle 11249	. . . . . 6 class ≤
33	31, 32	cop 4635	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
34		cds 17206	. . . . . . 7 class dist
35	2, 34	cfv 6544	. . . . . 6 class (dist‘ndx)
36	35, 26	cop 4635	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
37	29, 33, 36	ctp 4633	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
38		cunif 17207	. . . . . . 7 class UnifSet
39	2, 38	cfv 6544	. . . . . 6 class (UnifSet‘ndx)
40		cmetu 20935	. . . . . . 7 class metUnif
41	26, 40	cfv 6544	. . . . . 6 class (metUnif‘(abs ∘ − ))
42	39, 41	cop 4635	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
43	42	csn 4629	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
44	37, 43	cun 3947	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
45	21, 44	cun 3947	. 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  20946  cnfldbas  20948  cnfldadd  20949  cnfldmul  20950  cnfldcj  20951  cnfldtset  20952  cnfldle  20953  cnfldds  20954  cnfldunif  20955  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  cffldtocusgr  28704  gg-cnfldex  35180