Theorem lmodvscld

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

	Ref	Expression
Hypotheses	lmodvscld.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmodvscld.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmodvscld.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lmodvscld.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lmodvscld.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lmodvscld.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
	lmodvscld.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lmodvscld	⊢ ( 𝜑 → ( 𝑅 · 𝑋 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lmodvscld.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lmodvscld.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		lmodvscld.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		lmodvscld.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lmodvscld.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6		lmodvscld.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
7		lmodvscld.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8	1 2 3 4	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 )
9	5 6 7 8	syl3anc	⊢ ( 𝜑 → ( 𝑅 · 𝑋 ) ∈ 𝑉 )