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* ) |
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* ) |