Theorem nlmngp2

Description: The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypothesis	nlmnrg.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	nlmngp2	$$⊢W\in \mathrm{NrmMod}\to F\in \mathrm{NrmGrp}$$

Proof

Step	Hyp	Ref	Expression
1		nlmnrg.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2	1	nlmnrg	$$⊢W\in \mathrm{NrmMod}\to F\in \mathrm{NrmRing}$$
3		nrgngp	$$⊢F\in \mathrm{NrmRing}\to F\in \mathrm{NrmGrp}$$
4	2 3	syl	$$⊢W\in \mathrm{NrmMod}\to F\in \mathrm{NrmGrp}$$