Theorem nmhmcl

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

	Ref	Expression
Hypothesis	isnmhm2.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
Assertion	nmhmcl	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		isnmhm2.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2		nmhmnghm	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
3	1	nghmcl	⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
4	2 3	syl	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )