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 = ( Base ` W )
	clmvscl.f	|- F = ( Scalar ` W )
	clmvscl.s	|- .x. = ( .s ` W )
	clmvscl.k	|- K = ( Base ` F )
Assertion	clmvscl	|- ( ( W e. CMod /\ Q e. K /\ X e. V ) -> ( Q .x. X ) e. V )

Proof

Step	Hyp	Ref	Expression
1		clmvscl.v	|- V = ( Base ` W )
2		clmvscl.f	|- F = ( Scalar ` W )
3		clmvscl.s	|- .x. = ( .s ` W )
4		clmvscl.k	|- K = ( Base ` F )
5		clmlmod	|- ( W e. CMod -> W e. LMod )
6	1 2 3 4	lmodvscl	|- ( ( W e. LMod /\ Q e. K /\ X e. V ) -> ( Q .x. X ) e. V )
7	5 6	syl3an1	|- ( ( W e. CMod /\ Q e. K /\ X e. V ) -> ( Q .x. X ) e. V )