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 = norm CV ⁡ U
nmblolbi.5 ⊢ M = norm CV ⁡ W
nmblolbi.6 ⊢ N = U normOp OLD W
nmblolbi.7 ⊢ B = U BLnOp W
nmblolbi.u ⊢ U ∈ NrmCVec
nmblolbi.w ⊢ W ∈ NrmCVec
nmblolbii.b ⊢ T ∈ B
Assertion nmblolbii ⊢ A ∈ X → M ⁡ T ⁡ A ≤ N ⁡ T ⁢ L ⁡ A

Proof

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