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