Theorem clmvscl

Description: Closure of scalar product for a subcomplex module. Analogue of lmodvscl . (Contributed by NM, 3-Nov-2006) (Revised by AV, 28-Sep-2021)

	Ref	Expression
Hypotheses	clmvscl.v	$$⊢V={\mathrm{Base}}_W$$
	clmvscl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmvscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	clmvscl.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	clmvscl	$$⊢\left(W\in \mathrm{CMod}\wedge Q\in K\wedge X\in V\right)\to Q\underset{\dot{}}{·}X\in V$$

Proof

Step	Hyp	Ref	Expression
1		clmvscl.v	$$⊢V={\mathrm{Base}}_W$$
2		clmvscl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		clmvscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		clmvscl.k	$$⊢K={\mathrm{Base}}_F$$
5		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
6	1 2 3 4	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge Q\in K\wedge X\in V\right)\to Q\underset{\dot{}}{·}X\in V$$
7	5 6	syl3an1	$$⊢\left(W\in \mathrm{CMod}\wedge Q\in K\wedge X\in V\right)\to Q\underset{\dot{}}{·}X\in V$$