Theorem lmodvscld

Description: Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025)

	Ref	Expression
Hypotheses	lmodvscld.v	$$⊢V={\mathrm{Base}}_W$$
	lmodvscld.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmodvscld.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmodvscld.k	$$⊢K={\mathrm{Base}}_F$$
	lmodvscld.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lmodvscld.r	$$⊢\phi \to R\in K$$
	lmodvscld.x	$$⊢\phi \to X\in V$$
Assertion	lmodvscld	$$⊢\phi \to R\underset{\dot{}}{·}X\in V$$

Proof

Step	Hyp	Ref	Expression
1		lmodvscld.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodvscld.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		lmodvscld.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		lmodvscld.k	$$⊢K={\mathrm{Base}}_F$$
5		lmodvscld.w	$$⊢\phi \to W\in \mathrm{LMod}$$
6		lmodvscld.r	$$⊢\phi \to R\in K$$
7		lmodvscld.x	$$⊢\phi \to X\in V$$
8	1 2 3 4	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge R\in K\wedge X\in V\right)\to R\underset{\dot{}}{·}X\in V$$
9	5 6 7 8	syl3anc	$$⊢\phi \to R\underset{\dot{}}{·}X\in V$$