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=normCV⁡U
nmblolbi.5 ⊢M=normCV⁡W
nmblolbi.6 ⊢N=UnormOpOLDW
nmblolbi.7 ⊢B=UBLnOpW
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=normCV⁡U
3 nmblolbi.5 ⊢M=normCV⁡W
4 nmblolbi.6 ⊢N=UnormOpOLDW
5 nmblolbi.7 ⊢B=UBLnOpW
6 nmblolbi.u ⊢U∈NrmCVec
7 nmblolbi.w ⊢W∈NrmCVec
8 fveq1 ⊢T=ifT∈BTU0opW→T⁡A=ifT∈BTU0opW⁡A
9 8 fveq2d ⊢T=ifT∈BTU0opW→M⁡T⁡A=M⁡ifT∈BTU0opW⁡A
10 fveq2 ⊢T=ifT∈BTU0opW→N⁡T=N⁡ifT∈BTU0opW
11 10 oveq1d ⊢T=ifT∈BTU0opW→N⁡T⁢L⁡A=N⁡ifT∈BTU0opW⁢L⁡A
12 9 11 breq12d ⊢T=ifT∈BTU0opW→M⁡T⁡A≤N⁡T⁢L⁡A↔M⁡ifT∈BTU0opW⁡A≤N⁡ifT∈BTU0opW⁢L⁡A
13 12 imbi2d ⊢T=ifT∈BTU0opW→A∈X→M⁡T⁡A≤N⁡T⁢L⁡A↔A∈X→M⁡ifT∈BTU0opW⁡A≤N⁡ifT∈BTU0opW⁢L⁡A
14 eqid ⊢U0opW=U0opW
15 14 5 0blo ⊢U∈NrmCVec∧W∈NrmCVec→U0opW∈B
16 6 7 15 mp2an ⊢U0opW∈B
17 16 elimel ⊢ifT∈BTU0opW∈B
18 1 2 3 4 5 6 7 17 nmblolbii ⊢A∈X→M⁡ifT∈BTU0opW⁡A≤N⁡ifT∈BTU0opW⁢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