Metamath Proof Explorer

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 \in (S NGHom T) \to N (F) \in ℝ$

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2	1	isnghm	$⊢ F \in (S NGHom T) \leftrightarrow ((S \in NrmGrp \land T \in NrmGrp) \land (F \in (S GrpHom T) \land N (F) \in ℝ))$
3	2	simprbi	$⊢ F \in (S NGHom T) \to (F \in (S GrpHom T) \land N (F) \in ℝ)$
4	3	simprd	$⊢ F \in (S NGHom T) \to N (F) \in ℝ$