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