Metamath Proof Explorer


Theorem lvecgrp

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

Ref Expression
Assertion lvecgrp W LVec W Grp

Proof

Step Hyp Ref Expression
1 lveclmod W LVec W LMod
2 lmodgrp W LMod W Grp
3 1 2 syl W LVec W Grp