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 𝑋 = ( BaseSet ‘ 𝑈 )
nmblolbi.4 𝐿 = ( normCV𝑈 )
nmblolbi.5 𝑀 = ( normCV𝑊 )
nmblolbi.6 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmblolbi.7 𝐵 = ( 𝑈 BLnOp 𝑊 )
nmblolbi.u 𝑈 ∈ NrmCVec
nmblolbi.w 𝑊 ∈ NrmCVec
nmblolbii.b 𝑇𝐵
Assertion nmblolbii ( 𝐴𝑋 → ( 𝑀 ‘ ( 𝑇𝐴 ) ) ≤ ( ( 𝑁𝑇 ) · ( 𝐿𝐴 ) ) )

Proof

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