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) (New usage is discouraged.)

	Ref	Expression
Assertion	df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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		caddc	$$class+$$
9	7 8	cop	$$class⟨{+}_{\mathrm{ndx}},+⟩$$
10		cmulr	$$class{\cdot }_{𝑟}$$
11	2 10	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
12		cmul	$$class\times$$
13	11 12	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\times ⟩$$
14	5 9 13	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
15		cstv	$$class{\ast }_{𝑟}$$
16	2 15	cfv	$$class{\mathrm{*}}_{\mathrm{ndx}}$$
17		ccj	$$class*$$
18	16 17	cop	$$class⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩$$
19	18	csn	$$class\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
20	14 19	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
21		cts	$$class\mathrm{TopSet}$$
22	2 21	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
23		cmopn	$$class\mathrm{MetOpen}$$
24		cabs	$$class\mathrm{abs}$$
25		cmin	$$class-$$
26	24 25	ccom	$$class\left(\mathrm{abs}\circ -\right)$$
27	26 23	cfv	$$class\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
28	22 27	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩$$
29		cple	$$class\mathrm{le}$$
30	2 29	cfv	$$class{\le }_{\mathrm{ndx}}$$
31		cle	$$class\le$$
32	30 31	cop	$$class⟨{\le }_{\mathrm{ndx}},\le ⟩$$
33		cds	$$class\mathrm{dist}$$
34	2 33	cfv	$$class\mathrm{dist}\left(\mathrm{ndx}\right)$$
35	34 26	cop	$$class⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩$$
36	28 32 35	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\}$$
37		cunif	$$class\mathrm{UnifSet}$$
38	2 37	cfv	$$class\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
39		cmetu	$$class\mathrm{metUnif}$$
40	26 39	cfv	$$class\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$
41	38 40	cop	$$class⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩$$
42	41	csn	$$class\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
43	36 42	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)$$
44	20 43	cun	$$class\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)$$
45	0 44	wceq	$$wff{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)$$