Definition df-cnfld

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ` |``s restriction operator, for instance ( CCfld |`AA ) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex , cnfldadd , cnfldmul , cnfldcj , cnfldtset , cnfldle , cnfldds , and cnfldbas . 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) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025) (New usage is discouraged.)

	Ref	Expression
Assertion	df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
1		cbs	$$class\mathrm{Base}$$
2		cnx	$$class\mathrm{ndx}$$
3	2 1	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
4		cc	$$classℂ$$
5	3 4	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩$$
6		cplusg	$$class{+}_{𝑔}$$
7	2 6	cfv	$$class{+}_{\mathrm{ndx}}$$
8		vx	$$setvarx$$
9		vy	$$setvary$$
10	8	cv	$$setvarx$$
11		caddc	$$class+$$
12	9	cv	$$setvary$$
13	10 12 11	co	$$class\left(x+y\right)$$
14	8 9 4 4 13	cmpo	$$class\left(x\in ℂ,y\in ℂ⟼x+y\right)$$
15	7 14	cop	$$class⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩$$
16		cmulr	$$class{\cdot }_{𝑟}$$
17	2 16	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
18		cmul	$$class\times$$
19	10 12 18	co	$$classxy$$
20	8 9 4 4 19	cmpo	$$class\left(x\in ℂ,y\in ℂ⟼xy\right)$$
21	17 20	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩$$
22	5 15 21	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}$$
23		cstv	$$class{\ast }_{𝑟}$$
24	2 23	cfv	$$class{\mathrm{*}}_{\mathrm{ndx}}$$
25		ccj	$$class*$$
26	24 25	cop	$$class⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩$$
27	26	csn	$$class\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
28	22 27	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
29		cts	$$class\mathrm{TopSet}$$
30	2 29	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
31		cmopn	$$class\mathrm{MetOpen}$$
32		cabs	$$class\mathrm{abs}$$
33		cmin	$$class-$$
34	32 33	ccom	$$class\left(\mathrm{abs}\circ -\right)$$
35	34 31	cfv	$$class\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
36	30 35	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩$$
37		cple	$$class\mathrm{le}$$
38	2 37	cfv	$$class{\le }_{\mathrm{ndx}}$$
39		cle	$$class\le$$
40	38 39	cop	$$class⟨{\le }_{\mathrm{ndx}},\le ⟩$$
41		cds	$$class\mathrm{dist}$$
42	2 41	cfv	$$class\mathrm{dist}\left(\mathrm{ndx}\right)$$
43	42 34	cop	$$class⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩$$
44	36 40 43	ctp	$$class\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}$$
45		cunif	$$class\mathrm{UnifSet}$$
46	2 45	cfv	$$class\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
47		cmetu	$$class\mathrm{metUnif}$$
48	34 47	cfv	$$class\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$
49	46 48	cop	$$class⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩$$
50	49	csn	$$class\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
51	44 50	cun	$$class\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$
52	28 51	cun	$$class\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
53	0 52	wceq	$$wff{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$