Theorem cphclm

Description: A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Assertion	cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$

Proof

Step	Hyp	Ref	Expression
1		cphlmod	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{LMod}$$
2		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
4	2 3	cphsca	$$⊢W\in \mathrm{CPreHil}\to \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
5	2 3	cphsubrg	$$⊢W\in \mathrm{CPreHil}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
6	2 3	isclm	$$⊢W\in \mathrm{CMod}\leftrightarrow \left(W\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
7	1 4 5 6	syl3anbrc	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$