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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	lmodfgrp	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		lmodring.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2	1	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
3		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
4	2 3	syl	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )