Metamath Proof Explorer

Theorem nmogelb

Description: Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypotheses nmofval.1 
|- N = ( S normOp T )
nmofval.2 
|- V = ( Base ` S )
nmofval.3 
|- L = ( norm ` S )
nmofval.4 
|- M = ( norm ` T )
Assertion nmogelb 
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR* ) -> ( A <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> A <_ r ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 nmofval.2 
 |-  V = ( Base ` S )
3 nmofval.3 
 |-  L = ( norm ` S )
4 nmofval.4 
 |-  M = ( norm ` T )
5 1 2 3 4 nmoval 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
6 5 breq2d 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( A <_ ( N ` F ) <-> A <_ inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )
7 ssrab2 
 |-  { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ ( 0 [,) +oo )
8 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
9 7 8 sstri 
 |-  { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR*
10 infxrgelb 
 |-  ( ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR* /\ A e. RR* ) -> ( A <_ inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) <-> A. s e. { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } A <_ s ) )
11 9 10 mpan 
 |-  ( A e. RR* -> ( A <_ inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) <-> A. s e. { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } A <_ s ) )
12 breq2 
 |-  ( s = r -> ( A <_ s <-> A <_ r ) )
13 12 ralrab2 
 |-  ( A. s e. { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } A <_ s <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> A <_ r ) )
14 11 13 bitrdi 
 |-  ( A e. RR* -> ( A <_ inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> A <_ r ) ) )
15 6 14 sylan9bb 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR* ) -> ( A <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> A <_ r ) ) )