Metamath Proof Explorer

Theorem nghmghm

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

Ref Expression
Assertion nghmghm 
|- ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( S normOp T ) = ( S normOp T )
2 1 isnghm 
 |-  ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( ( S normOp T ) ` F ) e. RR ) ) )
3 2 simprbi 
 |-  ( F e. ( S NGHom T ) -> ( F e. ( S GrpHom T ) /\ ( ( S normOp T ) ` F ) e. RR ) )
4 3 simpld 
 |-  ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )