Theorem nmhmcl

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

	Ref	Expression
Hypothesis	isnmhm2.1	|- N = ( S normOp T )
Assertion	nmhmcl	|- ( F e. ( S NMHom T ) -> ( N ` F ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		isnmhm2.1	|- N = ( S normOp T )
2		nmhmnghm	|- ( F e. ( S NMHom T ) -> F e. ( S NGHom T ) )
3	1	nghmcl	|- ( F e. ( S NGHom T ) -> ( N ` F ) e. RR )
4	2 3	syl	|- ( F e. ( S NMHom T ) -> ( N ` F ) e. RR )