# Metamath Proof Explorer

## 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}},×⟩\right\}\cup \left\{⟨{*}_{\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}×$
13 11 12 cop ${class}⟨{\cdot }_{\mathrm{ndx}},×⟩$
14 5 9 13 ctp ${class}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}$
15 cstv ${class}{\ast }_{𝑟}$
16 2 15 cfv ${class}{*}_{\mathrm{ndx}}$
17 ccj ${class}*$
18 16 17 cop ${class}⟨{*}_{\mathrm{ndx}},*⟩$
19 18 csn ${class}\left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}$
20 14 19 cun ${class}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\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}},×⟩\right\}\cup \left\{⟨{*}_{\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}},×⟩\right\}\cup \left\{⟨{*}_{\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)$