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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑅 · 𝑋 ) ∈ 𝑉 )