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 e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )

Proof

Step Hyp Ref Expression
1 nmofval.1
 |-  N = ( S normOp T )
2 1 nmof
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* )
3 2 ffvelrnda
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
4 3 3impa
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )