Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
lmodgrpd
Next ⟩
lvecgrp
Metamath Proof Explorer
Ascii
Unicode
Theorem
lmodgrpd
Description:
A left module is a group.
(Contributed by
SN
, 16-May-2024)
Ref
Expression
Hypothesis
lmodgrpd.1
⊢
φ
→
W
∈
LMod
Assertion
lmodgrpd
⊢
φ
→
W
∈
Grp
Proof
Step
Hyp
Ref
Expression
1
lmodgrpd.1
⊢
φ
→
W
∈
LMod
2
lmodgrp
⊢
W
∈
LMod
→
W
∈
Grp
3
1
2
syl
⊢
φ
→
W
∈
Grp