Theorem nghmcl

Description: A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015)

	Ref	Expression
Hypothesis	nmofval.1	|- N = ( S normOp T )
Assertion	nghmcl	|- ( 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	simprbi	|- ( F e. ( S NGHom T ) -> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) )
4	3	simprd	|- ( F e. ( S NGHom T ) -> ( N ` F ) e. RR )