Metamath Proof Explorer

Theorem nmblolbii

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblolbi.1 
|- X = ( BaseSet ` U )
nmblolbi.4 
|- L = ( normCV ` U )
nmblolbi.5 
|- M = ( normCV ` W )
nmblolbi.6 
|- N = ( U normOpOLD W )
nmblolbi.7 
|- B = ( U BLnOp W )
nmblolbi.u 
|- U e. NrmCVec
nmblolbi.w 
|- W e. NrmCVec
nmblolbii.b 
|- T e. B
Assertion nmblolbii 
|- ( A e. X -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmblolbi.1 
 |-  X = ( BaseSet ` U )
2 nmblolbi.4 
 |-  L = ( normCV ` U )
3 nmblolbi.5 
 |-  M = ( normCV ` W )
4 nmblolbi.6 
 |-  N = ( U normOpOLD W )
5 nmblolbi.7 
 |-  B = ( U BLnOp W )
6 nmblolbi.u 
 |-  U e. NrmCVec
7 nmblolbi.w 
 |-  W e. NrmCVec
8 nmblolbii.b 
 |-  T e. B
9 fveq2 
 |-  ( A = ( 0vec ` U ) -> ( T ` A ) = ( T ` ( 0vec ` U ) ) )
10 9 fveq2d 
 |-  ( A = ( 0vec ` U ) -> ( M ` ( T ` A ) ) = ( M ` ( T ` ( 0vec ` U ) ) ) )
11 fveq2 
 |-  ( A = ( 0vec ` U ) -> ( L ` A ) = ( L ` ( 0vec ` U ) ) )
12 11 oveq2d 
 |-  ( A = ( 0vec ` U ) -> ( ( N ` T ) x. ( L ` A ) ) = ( ( N ` T ) x. ( L ` ( 0vec ` U ) ) ) )
13 10 12 breq12d 
 |-  ( A = ( 0vec ` U ) -> ( ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) <-> ( M ` ( T ` ( 0vec ` U ) ) ) <_ ( ( N ` T ) x. ( L ` ( 0vec ` U ) ) ) ) )
14 1 2 nvcl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( L ` A ) e. RR )
15 6 14 mpan 
 |-  ( A e. X -> ( L ` A ) e. RR )
16 15 adantr 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` A ) e. RR )
17 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
18 1 17 2 nvz 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( L ` A ) = 0 <-> A = ( 0vec ` U ) ) )
19 6 18 mpan 
 |-  ( A e. X -> ( ( L ` A ) = 0 <-> A = ( 0vec ` U ) ) )
20 19 necon3bid 
 |-  ( A e. X -> ( ( L ` A ) =/= 0 <-> A =/= ( 0vec ` U ) ) )
21 20 biimpar 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` A ) =/= 0 )
22 16 21 rereccld 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( 1 / ( L ` A ) ) e. RR )
23 1 17 2 nvgt0 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A =/= ( 0vec ` U ) <-> 0 < ( L ` A ) ) )
24 6 23 mpan 
 |-  ( A e. X -> ( A =/= ( 0vec ` U ) <-> 0 < ( L ` A ) ) )
25 24 biimpa 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> 0 < ( L ` A ) )
26 16 25 recgt0d 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> 0 < ( 1 / ( L ` A ) ) )
27 0re 
 |-  0 e. RR
28 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / ( L ` A ) ) e. RR ) -> ( 0 < ( 1 / ( L ` A ) ) -> 0 <_ ( 1 / ( L ` A ) ) ) )
29 27 22 28 sylancr 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( 0 < ( 1 / ( L ` A ) ) -> 0 <_ ( 1 / ( L ` A ) ) ) )
30 26 29 mpd 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> 0 <_ ( 1 / ( L ` A ) ) )
31 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
32 1 31 5 blof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T : X --> ( BaseSet ` W ) )
33 6 7 8 32 mp3an 
 |-  T : X --> ( BaseSet ` W )
34 33 ffvelrni 
 |-  ( A e. X -> ( T ` A ) e. ( BaseSet ` W ) )
35 34 adantr 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( T ` A ) e. ( BaseSet ` W ) )
36 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
37 31 36 3 nvsge0 
 |-  ( ( W e. NrmCVec /\ ( ( 1 / ( L ` A ) ) e. RR /\ 0 <_ ( 1 / ( L ` A ) ) ) /\ ( T ` A ) e. ( BaseSet ` W ) ) -> ( M ` ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) ) = ( ( 1 / ( L ` A ) ) x. ( M ` ( T ` A ) ) ) )
38 7 37 mp3an1 
 |-  ( ( ( ( 1 / ( L ` A ) ) e. RR /\ 0 <_ ( 1 / ( L ` A ) ) ) /\ ( T ` A ) e. ( BaseSet ` W ) ) -> ( M ` ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) ) = ( ( 1 / ( L ` A ) ) x. ( M ` ( T ` A ) ) ) )
39 22 30 35 38 syl21anc 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( M ` ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) ) = ( ( 1 / ( L ` A ) ) x. ( M ` ( T ` A ) ) ) )
40 22 recnd 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( 1 / ( L ` A ) ) e. CC )
41 simpl 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> A e. X )
42 eqid 
 |-  ( U LnOp W ) = ( U LnOp W )
43 42 5 bloln 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. ( U LnOp W ) )
44 6 7 8 43 mp3an 
 |-  T e. ( U LnOp W )
45 6 7 44 3pm3.2i 
 |-  ( U e. NrmCVec /\ W e. NrmCVec /\ T e. ( U LnOp W ) )
46 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
47 1 46 36 42 lnomul 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. ( U LnOp W ) ) /\ ( ( 1 / ( L ` A ) ) e. CC /\ A e. X ) ) -> ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) = ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) )
48 45 47 mpan 
 |-  ( ( ( 1 / ( L ` A ) ) e. CC /\ A e. X ) -> ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) = ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) )
49 40 41 48 syl2anc 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) = ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) )
50 49 fveq2d 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( M ` ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) ) = ( M ` ( ( 1 / ( L ` A ) ) ( .sOLD ` W ) ( T ` A ) ) ) )
51 31 3 nvcl 
 |-  ( ( W e. NrmCVec /\ ( T ` A ) e. ( BaseSet ` W ) ) -> ( M ` ( T ` A ) ) e. RR )
52 7 34 51 sylancr 
 |-  ( A e. X -> ( M ` ( T ` A ) ) e. RR )
53 52 adantr 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( M ` ( T ` A ) ) e. RR )
54 53 recnd 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( M ` ( T ` A ) ) e. CC )
55 16 recnd 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` A ) e. CC )
56 54 55 21 divrec2d 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( ( M ` ( T ` A ) ) / ( L ` A ) ) = ( ( 1 / ( L ` A ) ) x. ( M ` ( T ` A ) ) ) )
57 39 50 56 3eqtr4rd 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( ( M ` ( T ` A ) ) / ( L ` A ) ) = ( M ` ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) ) )
58 1 46 nvscl 
 |-  ( ( U e. NrmCVec /\ ( 1 / ( L ` A ) ) e. CC /\ A e. X ) -> ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X )
59 6 58 mp3an1 
 |-  ( ( ( 1 / ( L ` A ) ) e. CC /\ A e. X ) -> ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X )
60 59 ancoms 
 |-  ( ( A e. X /\ ( 1 / ( L ` A ) ) e. CC ) -> ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X )
61 40 60 syldan 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X )
62 1 2 nvcl 
 |-  ( ( U e. NrmCVec /\ ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X ) -> ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) e. RR )
63 6 61 62 sylancr 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) e. RR )
64 1 46 17 2 nv1 
 |-  ( ( U e. NrmCVec /\ A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) = 1 )
65 6 64 mp3an1 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) = 1 )
66 eqle 
 |-  ( ( ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) e. RR /\ ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) = 1 ) -> ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) <_ 1 )
67 63 65 66 syl2anc 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) <_ 1 )
68 6 7 33 3pm3.2i 
 |-  ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> ( BaseSet ` W ) )
69 1 31 2 3 4 nmoolb 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> ( BaseSet ` W ) ) /\ ( ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X /\ ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) <_ 1 ) ) -> ( M ` ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) ) <_ ( N ` T ) )
70 68 69 mpan 
 |-  ( ( ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) e. X /\ ( L ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) <_ 1 ) -> ( M ` ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) ) <_ ( N ` T ) )
71 61 67 70 syl2anc 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( M ` ( T ` ( ( 1 / ( L ` A ) ) ( .sOLD ` U ) A ) ) ) <_ ( N ` T ) )
72 57 71 eqbrtrd 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( ( M ` ( T ` A ) ) / ( L ` A ) ) <_ ( N ` T ) )
73 1 31 4 5 nmblore 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( N ` T ) e. RR )
74 6 7 8 73 mp3an 
 |-  ( N ` T ) e. RR
75 74 a1i 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( N ` T ) e. RR )
76 ledivmul2 
 |-  ( ( ( M ` ( T ` A ) ) e. RR /\ ( N ` T ) e. RR /\ ( ( L ` A ) e. RR /\ 0 < ( L ` A ) ) ) -> ( ( ( M ` ( T ` A ) ) / ( L ` A ) ) <_ ( N ` T ) <-> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) ) )
77 53 75 16 25 76 syl112anc 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( ( ( M ` ( T ` A ) ) / ( L ` A ) ) <_ ( N ` T ) <-> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) ) )
78 72 77 mpbid 
 |-  ( ( A e. X /\ A =/= ( 0vec ` U ) ) -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) )
79 0le0 
 |-  0 <_ 0
80 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
81 1 31 17 80 42 lno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. ( U LnOp W ) ) -> ( T ` ( 0vec ` U ) ) = ( 0vec ` W ) )
82 6 7 44 81 mp3an 
 |-  ( T ` ( 0vec ` U ) ) = ( 0vec ` W )
83 82 fveq2i 
 |-  ( M ` ( T ` ( 0vec ` U ) ) ) = ( M ` ( 0vec ` W ) )
84 80 3 nvz0 
 |-  ( W e. NrmCVec -> ( M ` ( 0vec ` W ) ) = 0 )
85 7 84 ax-mp 
 |-  ( M ` ( 0vec ` W ) ) = 0
86 83 85 eqtri 
 |-  ( M ` ( T ` ( 0vec ` U ) ) ) = 0
87 17 2 nvz0 
 |-  ( U e. NrmCVec -> ( L ` ( 0vec ` U ) ) = 0 )
88 6 87 ax-mp 
 |-  ( L ` ( 0vec ` U ) ) = 0
89 88 oveq2i 
 |-  ( ( N ` T ) x. ( L ` ( 0vec ` U ) ) ) = ( ( N ` T ) x. 0 )
90 74 recni 
 |-  ( N ` T ) e. CC
91 90 mul01i 
 |-  ( ( N ` T ) x. 0 ) = 0
92 89 91 eqtri 
 |-  ( ( N ` T ) x. ( L ` ( 0vec ` U ) ) ) = 0
93 79 86 92 3brtr4i 
 |-  ( M ` ( T ` ( 0vec ` U ) ) ) <_ ( ( N ` T ) x. ( L ` ( 0vec ` U ) ) )
94 93 a1i 
 |-  ( A e. X -> ( M ` ( T ` ( 0vec ` U ) ) ) <_ ( ( N ` T ) x. ( L ` ( 0vec ` U ) ) ) )
95 13 78 94 pm2.61ne 
 |-  ( A e. X -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) )