Metamath Proof Explorer


Theorem lvecgrpd

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

Ref Expression
Hypothesis lveclmodd.1 φ W LVec
Assertion lvecgrpd φ W Grp

Proof

Step Hyp Ref Expression
1 lveclmodd.1 φ W LVec
2 1 lveclmodd φ W LMod
3 2 lmodgrpd φ W Grp