Description: A vector space is a group. (Contributed by SN, 16-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lveclmodd.1 | |- ( ph -> W e. LVec ) |
|
Assertion | lvecgrpd | |- ( ph -> W e. Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lveclmodd.1 | |- ( ph -> W e. LVec ) |
|
2 | 1 | lveclmodd | |- ( ph -> W e. LMod ) |
3 | 2 | lmodgrpd | |- ( ph -> W e. Grp ) |