Description: A vector space is a group. (Contributed by SN, 28-May-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | lvecgrp | |- ( W e. LVec -> W e. Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lveclmod | |- ( W e. LVec -> W e. LMod ) |
|
2 | 1 | lmodgrpd | |- ( W e. LVec -> W e. Grp ) |