Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
lvecgrp
Next ⟩
lvecring
Metamath Proof Explorer
Ascii
Structured
Theorem
lvecgrp
Description:
A vector space is a group.
(Contributed by
SN
, 28-May-2023)
Ref
Expression
Assertion
lvecgrp
⊢
(
𝑊
∈ LVec →
𝑊
∈ Grp )
Proof
Step
Hyp
Ref
Expression
1
lveclmod
⊢
(
𝑊
∈ LVec →
𝑊
∈ LMod )
2
1
lmodgrpd
⊢
(
𝑊
∈ LVec →
𝑊
∈ Grp )