Metamath Proof Explorer


Theorem lveclmodd

Description: A vector space is a left module. (Contributed by SN, 16-May-2024)

Ref Expression
Hypothesis lveclmodd.1 ( 𝜑𝑊 ∈ LVec )
Assertion lveclmodd ( 𝜑𝑊 ∈ LMod )

Proof

Step Hyp Ref Expression
1 lveclmodd.1 ( 𝜑𝑊 ∈ LVec )
2 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
3 1 2 syl ( 𝜑𝑊 ∈ LMod )