Theorem lvecgrpd

Description: A vector space is a group. (Contributed by SN, 16-May-2024)

	Ref	Expression
Hypothesis	lvecgrpd.1	$$⊢\phi \to W\in \mathrm{LVec}$$
Assertion	lvecgrpd	$$⊢\phi \to W\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		lvecgrpd.1	$$⊢\phi \to W\in \mathrm{LVec}$$
2	1	lveclmodd	$$⊢\phi \to W\in \mathrm{LMod}$$
3	2	lmodgrpd	$$⊢\phi \to W\in \mathrm{Grp}$$