Theorem lmodfgrp

Description: The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypothesis	lmodring.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	lmodfgrp	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		lmodring.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2	1	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
3		ringgrp	$$⊢F\in \mathrm{Ring}\to F\in \mathrm{Grp}$$
4	2 3	syl	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Grp}$$