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 
|- F = ( Scalar ` W )
Assertion nlmngp2 
|- ( W e. NrmMod -> F e. NrmGrp )

Proof

Step Hyp Ref Expression
1 nlmnrg.1 
 |-  F = ( Scalar ` W )
2 1 nlmnrg 
 |-  ( W e. NrmMod -> F e. NrmRing )
3 nrgngp 
 |-  ( F e. NrmRing -> F e. NrmGrp )
4 2 3 syl 
 |-  ( W e. NrmMod -> F e. NrmGrp )