Metamath Proof Explorer

Theorem nmolb

Description: Any upper bound on the values of a linear operator translates to an upper bound on 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 nmolb 
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )

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 elrege0 
 |-  ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
6 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* , < ) )
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 infxrcl 
 |-  ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR* -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. RR* )
11 9 10 mp1i 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. RR* )
12 6 11 eqeltrd 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
13 12 xrleidd 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) <_ ( N ` F ) )
14 1 2 3 4 nmogelb 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) e. RR* ) -> ( ( N ` F ) <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) ) )
15 12 14 mpdan 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) ) )
16 13 15 mpbid 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) )
17 oveq1 
 |-  ( r = A -> ( r x. ( L ` x ) ) = ( A x. ( L ` x ) ) )
18 17 breq2d 
 |-  ( r = A -> ( ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) <-> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
19 18 ralbidv 
 |-  ( r = A -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) <-> A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
20 breq2 
 |-  ( r = A -> ( ( N ` F ) <_ r <-> ( N ` F ) <_ A ) )
21 19 20 imbi12d 
 |-  ( r = A -> ( ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) <-> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) )
22 21 rspccv 
 |-  ( A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) -> ( A e. ( 0 [,) +oo ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) )
23 16 22 syl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( A e. ( 0 [,) +oo ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) )
24 5 23 syl5bir 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) )
25 24 3impib 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )