This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) ∈ 𝑉 )