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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	nlmngp2	⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )

Proof

Step	Hyp	Ref	Expression
1		nlmnrg.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2	1	nlmnrg	⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing )
3		nrgngp	⊢ ( 𝐹 ∈ NrmRing → 𝐹 ∈ NrmGrp )
4	2 3	syl	⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )