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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	clmvscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clmvscl.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	clmvscl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmvscl	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		clmvscl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		clmvscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		clmvscl.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		clmvscl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
6	1 2 3 4	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) ∈ 𝑉 )
7	5 6	syl3an1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) ∈ 𝑉 )