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 1 lmodgrpd W LVec W Grp