Metamath Proof Explorer

Theorem nmlnoubi

Description: An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nmlnoubi.1 
|- X = ( BaseSet ` U )
nmlnoubi.z 
|- Z = ( 0vec ` U )
nmlnoubi.k 
|- K = ( normCV ` U )
nmlnoubi.m 
|- M = ( normCV ` W )
nmlnoubi.3 
|- N = ( U normOpOLD W )
nmlnoubi.7 
|- L = ( U LnOp W )
nmlnoubi.u 
|- U e. NrmCVec
nmlnoubi.w 
|- W e. NrmCVec
Assertion nmlnoubi 
|- ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) ) -> ( N ` T ) <_ A )

Proof

Step Hyp Ref Expression
1 nmlnoubi.1 
 |-  X = ( BaseSet ` U )
2 nmlnoubi.z 
 |-  Z = ( 0vec ` U )
3 nmlnoubi.k 
 |-  K = ( normCV ` U )
4 nmlnoubi.m 
 |-  M = ( normCV ` W )
5 nmlnoubi.3 
 |-  N = ( U normOpOLD W )
6 nmlnoubi.7 
 |-  L = ( U LnOp W )
7 nmlnoubi.u 
 |-  U e. NrmCVec
8 nmlnoubi.w 
 |-  W e. NrmCVec
9 2fveq3 
 |-  ( x = Z -> ( M ` ( T ` x ) ) = ( M ` ( T ` Z ) ) )
10 fveq2 
 |-  ( x = Z -> ( K ` x ) = ( K ` Z ) )
11 10 oveq2d 
 |-  ( x = Z -> ( A x. ( K ` x ) ) = ( A x. ( K ` Z ) ) )
12 9 11 breq12d 
 |-  ( x = Z -> ( ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) <-> ( M ` ( T ` Z ) ) <_ ( A x. ( K ` Z ) ) ) )
13 id 
 |-  ( ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) -> ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) )
14 13 imp 
 |-  ( ( ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) /\ x =/= Z ) -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) )
15 14 adantll 
 |-  ( ( ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) /\ ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) ) /\ x =/= Z ) -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) )
16 0le0 
 |-  0 <_ 0
17 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
18 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
19 1 17 2 18 6 lno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Z ) = ( 0vec ` W ) )
20 7 8 19 mp3an12 
 |-  ( T e. L -> ( T ` Z ) = ( 0vec ` W ) )
21 20 fveq2d 
 |-  ( T e. L -> ( M ` ( T ` Z ) ) = ( M ` ( 0vec ` W ) ) )
22 18 4 nvz0 
 |-  ( W e. NrmCVec -> ( M ` ( 0vec ` W ) ) = 0 )
23 8 22 ax-mp 
 |-  ( M ` ( 0vec ` W ) ) = 0
24 21 23 eqtrdi 
 |-  ( T e. L -> ( M ` ( T ` Z ) ) = 0 )
25 24 adantr 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) -> ( M ` ( T ` Z ) ) = 0 )
26 2 3 nvz0 
 |-  ( U e. NrmCVec -> ( K ` Z ) = 0 )
27 7 26 ax-mp 
 |-  ( K ` Z ) = 0
28 27 oveq2i 
 |-  ( A x. ( K ` Z ) ) = ( A x. 0 )
29 recn 
 |-  ( A e. RR -> A e. CC )
30 29 mul01d 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
31 28 30 syl5eq 
 |-  ( A e. RR -> ( A x. ( K ` Z ) ) = 0 )
32 31 ad2antrl 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) -> ( A x. ( K ` Z ) ) = 0 )
33 25 32 breq12d 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) -> ( ( M ` ( T ` Z ) ) <_ ( A x. ( K ` Z ) ) <-> 0 <_ 0 ) )
34 16 33 mpbiri 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) -> ( M ` ( T ` Z ) ) <_ ( A x. ( K ` Z ) ) )
35 34 adantr 
 |-  ( ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) /\ ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) ) -> ( M ` ( T ` Z ) ) <_ ( A x. ( K ` Z ) ) )
36 12 15 35 pm2.61ne 
 |-  ( ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) /\ ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) ) -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) )
37 36 ex 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) -> ( ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) )
38 37 ralimdv 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) ) -> ( A. x e. X ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) -> A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) )
39 38 3impia 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) ) -> A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) )
40 1 17 6 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
41 7 8 40 mp3an12 
 |-  ( T e. L -> T : X --> ( BaseSet ` W ) )
42 1 17 3 4 5 7 8 nmoub2i 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) -> ( N ` T ) <_ A )
43 41 42 syl3an1 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) -> ( N ` T ) <_ A )
44 39 43 syld3an3 
 |-  ( ( T e. L /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( x =/= Z -> ( M ` ( T ` x ) ) <_ ( A x. ( K ` x ) ) ) ) -> ( N ` T ) <_ A )