Theorem isnghm2

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

	Ref	Expression
Hypothesis	nmofval.1	|- N = ( S normOp T )
Assertion	isnghm2	|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	|- N = ( S normOp T )
2	1	isnghm	|- ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
3	2	baib	|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( F e. ( S NGHom T ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
4	3	baibd	|- ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
5	4	3impa	|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )