Metamath Proof Explorer


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 )