Metamath Proof Explorer


Theorem phllmod

Description: A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Assertion phllmod ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )

Proof

Step Hyp Ref Expression
1 phllvec ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )
2 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
3 1 2 syl ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )