Metamath Proof Explorer

Theorem nmof

Description: The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypothesis nmofval.1 
|- N = ( S normOp T )
Assertion nmof 
|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 eqid 
 |-  ( Base ` S ) = ( Base ` S )
3 eqid 
 |-  ( norm ` S ) = ( norm ` S )
4 eqid 
 |-  ( norm ` T ) = ( norm ` T )
5 1 2 3 4 nmofval 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` S ) ( ( norm ` T ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) } , RR* , < ) ) )
6 ssrab2 
 |-  { r e. ( 0 [,) +oo ) | A. x e. ( Base ` S ) ( ( norm ` T ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) } C_ ( 0 [,) +oo )
7 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
8 6 7 sstri 
 |-  { r e. ( 0 [,) +oo ) | A. x e. ( Base ` S ) ( ( norm ` T ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) } C_ RR*
9 infxrcl 
 |-  ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` S ) ( ( norm ` T ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) } C_ RR* -> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` S ) ( ( norm ` T ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) } , RR* , < ) e. RR* )
10 8 9 mp1i 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ f e. ( S GrpHom T ) ) -> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` S ) ( ( norm ` T ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) } , RR* , < ) e. RR* )
11 5 10 fmpt3d 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* )