Metamath Proof Explorer

Theorem lvecgrp

Description: A left vector is a group. (Contributed by Steven Nguyen, 28-May-2023)

Ref Expression
Assertion lvecgrp ⊢ W ∈ LVec → W ∈ Grp

Proof

Step Hyp Ref Expression
1 lveclmod ⊢ W ∈ LVec → W ∈ LMod
2 lmodgrp ⊢ W ∈ LMod → W ∈ Grp
3 1 2 syl ⊢ W ∈ LVec → W ∈ Grp