Theorem cphcjcl

Description: The scalar field of a subcomplex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015)

	Ref	Expression
Hypotheses	cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cphsca.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cphcjcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\right)\to \bar{A}\in K$$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		cphsca.k	$$⊢K={\mathrm{Base}}_F$$
3	1 2	cphsca	$$⊢W\in \mathrm{CPreHil}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
4	3	fveq2d	$$⊢W\in \mathrm{CPreHil}\to {\mathrm{*}}_F={\mathrm{*}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
5	2	fvexi	$$⊢K\in \mathrm{V}$$
6		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
7		cnfldcj	$$⊢*={\mathrm{*}}_{{ℂ}_{\mathrm{fld}}}$$
8	6 7	ressstarv	$$⊢K\in \mathrm{V}\to *={\mathrm{*}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
9	5 8	ax-mp	$$⊢*={\mathrm{*}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
10	4 9	eqtr4di	$$⊢W\in \mathrm{CPreHil}\to {\mathrm{*}}_F=*$$
11	10	adantr	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\right)\to {\mathrm{*}}_F=*$$
12	11	fveq1d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\right)\to A^{{\mathrm{*}}_F}=\bar{A}$$
13		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
14	1	phlsrng	$$⊢W\in \mathrm{PreHil}\to F\in \mathrm{*-Ring}$$
15	13 14	syl	$$⊢W\in \mathrm{CPreHil}\to F\in \mathrm{*-Ring}$$
16		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
17	16 2	srngcl	$$⊢\left(F\in \mathrm{*-Ring}\wedge A\in K\right)\to A^{{\mathrm{*}}_F}\in K$$
18	15 17	sylan	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\right)\to A^{{\mathrm{*}}_F}\in K$$
19	12 18	eqeltrrd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\right)\to \bar{A}\in K$$