Theorem phclm

Description: A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphcph.v	$$⊢V={\mathrm{Base}}_W$$
	tcphcph.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	tcphcph.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
	tcphcph.2	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
Assertion	phclm	$$⊢\phi \to W\in \mathrm{CMod}$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphcph.v	$$⊢V={\mathrm{Base}}_W$$
3		tcphcph.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		tcphcph.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
5		tcphcph.2	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
6		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
7	4 6	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
8		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
9		phllvec	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LVec}$$
10	4 9	syl	$$⊢\phi \to W\in \mathrm{LVec}$$
11	3	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
12	10 11	syl	$$⊢\phi \to F\in \mathrm{DivRing}$$
13	8 5 12	cphsubrglem	$$⊢\phi \to \left(F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\wedge {\mathrm{Base}}_F=K\cap ℂ\wedge {\mathrm{Base}}_F\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
14	13	simp1d	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
15	13	simp3d	$$⊢\phi \to {\mathrm{Base}}_F\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
16	3 8	isclm	$$⊢W\in \mathrm{CMod}\leftrightarrow \left(W\in \mathrm{LMod}\wedge F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\wedge {\mathrm{Base}}_F\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
17	7 14 15 16	syl3anbrc	$$⊢\phi \to W\in \mathrm{CMod}$$