Metamath Proof Explorer


Theorem lvecgrpd

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

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

Proof

Step Hyp Ref Expression
1 lveclmodd.1 ( 𝜑𝑊 ∈ LVec )
2 1 lveclmodd ( 𝜑𝑊 ∈ LMod )
3 2 lmodgrpd ( 𝜑𝑊 ∈ Grp )