Theorem cnfldcj

Description: The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 17-Dec-2017)

	Ref	Expression
Assertion	cnfldcj	$$⊢*={\mathrm{*}}_{{ℂ}_{\mathrm{fld}}}$$

Proof

Step	Hyp	Ref	Expression
1		cjf	$$⊢*:ℂ⟶ℂ$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3		fex2	$$⊢\left(*:ℂ⟶ℂ\wedge ℂ\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to *\in \mathrm{V}$$
4	1 2 2 3	mp3an	$$⊢*\in \mathrm{V}$$
5		cnfldstr	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$$
6		starvid	$$⊢{\ast }_{𝑟}=\mathrm{Slot}{\mathrm{*}}_{\mathrm{ndx}}$$
7		ssun2	$$⊢\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
8		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq \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)$$
9		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)$$
10	8 9	sseqtrri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$$
11	7 10	sstri	$$⊢\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$$
12	5 6 11	strfv	$$⊢*\in \mathrm{V}\to *={\mathrm{*}}_{{ℂ}_{\mathrm{fld}}}$$
13	4 12	ax-mp	$$⊢*={\mathrm{*}}_{{ℂ}_{\mathrm{fld}}}$$