Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
lvecgrpd
Next ⟩
lvecring
Metamath Proof Explorer
Ascii
Unicode
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