Metamath Proof Explorer

Theorem nlmngp

Description: A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion nlmngp 
|- ( W e. NrmMod -> W e. NrmGrp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 eqid 
 |-  ( norm ` W ) = ( norm ` W )
3 eqid 
 |-  ( .s ` W ) = ( .s ` W )
4 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
5 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
6 eqid 
 |-  ( norm ` ( Scalar ` W ) ) = ( norm ` ( Scalar ` W ) )
7 1 2 3 4 5 6 isnlm 
 |-  ( W e. NrmMod <-> ( ( W e. NrmGrp /\ W e. LMod /\ ( Scalar ` W ) e. NrmRing ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( Base ` W ) ( ( norm ` W ) ` ( x ( .s ` W ) y ) ) = ( ( ( norm ` ( Scalar ` W ) ) ` x ) x. ( ( norm ` W ) ` y ) ) ) )
8 7 simplbi 
 |-  ( W e. NrmMod -> ( W e. NrmGrp /\ W e. LMod /\ ( Scalar ` W ) e. NrmRing ) )
9 8 simp1d 
 |-  ( W e. NrmMod -> W e. NrmGrp )