Metamath Proof Explorer

Theorem nmocl

Description: The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015)

		Ref	Expression
	Hypothesis	nmofval.1	$⊢ N = S normOp T$
	Assertion	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2	1	nmof	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N : S GrpHom T ⟶ ℝ^{*}$
3	2	ffvelcdmda	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
4	3	3impa	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$