Metamath Proof Explorer

Theorem lvecgrp

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

Ref Expression
Assertion lvecgrp 
|- ( W e. LVec -> W e. Grp )

Proof

Step Hyp Ref Expression
1 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
2 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
3 1 2 syl 
 |-  ( W e. LVec -> W e. Grp )