Metamath Proof Explorer

Theorem nmblolbi

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-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
Assertion nmblolbi ⊢ T ∈ B ∧ 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 fveq1 ⊢ T = if T ∈ B T U 0 op W → T ⁡ A = if T ∈ B T U 0 op W ⁡ A
9 8 fveq2d ⊢ T = if T ∈ B T U 0 op W → M ⁡ T ⁡ A = M ⁡ if T ∈ B T U 0 op W ⁡ A
10 fveq2 ⊢ T = if T ∈ B T U 0 op W → N ⁡ T = N ⁡ if T ∈ B T U 0 op W
11 10 oveq1d ⊢ T = if T ∈ B T U 0 op W → N ⁡ T ⁢ L ⁡ A = N ⁡ if T ∈ B T U 0 op W ⁢ L ⁡ A
12 9 11 breq12d ⊢ T = if T ∈ B T U 0 op W → M ⁡ T ⁡ A ≤ N ⁡ T ⁢ L ⁡ A ↔ M ⁡ if T ∈ B T U 0 op W ⁡ A ≤ N ⁡ if T ∈ B T U 0 op W ⁢ L ⁡ A
13 12 imbi2d ⊢ T = if T ∈ B T U 0 op W → A ∈ X → M ⁡ T ⁡ A ≤ N ⁡ T ⁢ L ⁡ A ↔ A ∈ X → M ⁡ if T ∈ B T U 0 op W ⁡ A ≤ N ⁡ if T ∈ B T U 0 op W ⁢ L ⁡ A
14 eqid ⊢ U 0 op W = U 0 op W
15 14 5 0blo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U 0 op W ∈ B
16 6 7 15 mp2an ⊢ U 0 op W ∈ B
17 16 elimel ⊢ if T ∈ B T U 0 op W ∈ B
18 1 2 3 4 5 6 7 17 nmblolbii ⊢ A ∈ X → M ⁡ if T ∈ B T U 0 op W ⁡ A ≤ N ⁡ if T ∈ B T U 0 op W ⁢ L ⁡ A
19 13 18 dedth ⊢ T ∈ B → A ∈ X → M ⁡ T ⁡ A ≤ N ⁡ T ⁢ L ⁡ A
20 19 imp ⊢ T ∈ B ∧ A ∈ X → M ⁡ T ⁡ A ≤ N ⁡ T ⁢ L ⁡ A