Theorem cphsca

Description: A subcomplex pre-Hilbert space is a vector space over a subfield of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cphsca.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cphsca	$$⊢W\in \mathrm{CPreHil}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		cphsca.k	$$⊢K={\mathrm{Base}}_F$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
5		eqid	$$⊢\mathrm{norm}\left(W\right)=\mathrm{norm}\left(W\right)$$
6	3 4 5 1 2	iscph	$$⊢W\in \mathrm{CPreHil}\leftrightarrow \left(\left(W\in \mathrm{PreHil}\wedge W\in \mathrm{NrmMod}\wedge F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)\wedge \surd \left[K\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq K\wedge \mathrm{norm}\left(W\right)=\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\right)$$
7	6	simp1bi	$$⊢W\in \mathrm{CPreHil}\to \left(W\in \mathrm{PreHil}\wedge W\in \mathrm{NrmMod}\wedge F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)$$
8	7	simp3d	$$⊢W\in \mathrm{CPreHil}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$