Metamath Proof Explorer


Theorem lvecgrpd

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

Ref Expression
Hypothesis lveclmodd.1
|- ( ph -> W e. LVec )
Assertion lvecgrpd
|- ( ph -> W e. Grp )

Proof

Step Hyp Ref Expression
1 lveclmodd.1
 |-  ( ph -> W e. LVec )
2 1 lveclmodd
 |-  ( ph -> W e. LMod )
3 2 lmodgrpd
 |-  ( ph -> W e. Grp )