Metamath Proof Explorer

Theorem nmoolb

Description: A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoolb.1 ⊢X=BaseSet⁡U
nmoolb.2 ⊢Y=BaseSet⁡W
nmoolb.l ⊢L=normCV⁡U
nmoolb.m ⊢M=normCV⁡W
nmoolb.3 ⊢N=UnormOpOLDW
Assertion nmoolb ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y∧A∈X∧L⁡A≤1→M⁡T⁡A≤N⁡T

Proof

Step Hyp Ref Expression
1 nmoolb.1 ⊢X=BaseSet⁡U
2 nmoolb.2 ⊢Y=BaseSet⁡W
3 nmoolb.l ⊢L=normCV⁡U
4 nmoolb.m ⊢M=normCV⁡W
5 nmoolb.3 ⊢N=UnormOpOLDW
6 2 4 nmosetre ⊢W∈NrmCVec∧T:X⟶Y→x|∃y∈XL⁡y≤1∧x=M⁡T⁡y⊆ℝ
7 ressxr ⊢ℝ⊆ℝ*
8 6 7 sstrdi ⊢W∈NrmCVec∧T:X⟶Y→x|∃y∈XL⁡y≤1∧x=M⁡T⁡y⊆ℝ*
9 8 3adant1 ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→x|∃y∈XL⁡y≤1∧x=M⁡T⁡y⊆ℝ*
10 fveq2 ⊢y=A→L⁡y=L⁡A
11 10 breq1d ⊢y=A→L⁡y≤1↔L⁡A≤1
12 2fveq3 ⊢y=A→M⁡T⁡y=M⁡T⁡A
13 12 eqeq2d ⊢y=A→M⁡T⁡A=M⁡T⁡y↔M⁡T⁡A=M⁡T⁡A
14 11 13 anbi12d ⊢y=A→L⁡y≤1∧M⁡T⁡A=M⁡T⁡y↔L⁡A≤1∧M⁡T⁡A=M⁡T⁡A
15 eqid ⊢M⁡T⁡A=M⁡T⁡A
16 15 biantru ⊢L⁡A≤1↔L⁡A≤1∧M⁡T⁡A=M⁡T⁡A
17 14 16 bitr4di ⊢y=A→L⁡y≤1∧M⁡T⁡A=M⁡T⁡y↔L⁡A≤1
18 17 rspcev ⊢A∈X∧L⁡A≤1→∃y∈XL⁡y≤1∧M⁡T⁡A=M⁡T⁡y
19 fvex ⊢M⁡T⁡A∈V
20 eqeq1 ⊢x=M⁡T⁡A→x=M⁡T⁡y↔M⁡T⁡A=M⁡T⁡y
21 20 anbi2d ⊢x=M⁡T⁡A→L⁡y≤1∧x=M⁡T⁡y↔L⁡y≤1∧M⁡T⁡A=M⁡T⁡y
22 21 rexbidv ⊢x=M⁡T⁡A→∃y∈XL⁡y≤1∧x=M⁡T⁡y↔∃y∈XL⁡y≤1∧M⁡T⁡A=M⁡T⁡y
23 19 22 elab ⊢M⁡T⁡A∈x|∃y∈XL⁡y≤1∧x=M⁡T⁡y↔∃y∈XL⁡y≤1∧M⁡T⁡A=M⁡T⁡y
24 18 23 sylibr ⊢A∈X∧L⁡A≤1→M⁡T⁡A∈x|∃y∈XL⁡y≤1∧x=M⁡T⁡y
25 supxrub ⊢x|∃y∈XL⁡y≤1∧x=M⁡T⁡y⊆ℝ*∧M⁡T⁡A∈x|∃y∈XL⁡y≤1∧x=M⁡T⁡y→M⁡T⁡A≤supx|∃y∈XL⁡y≤1∧x=M⁡T⁡yℝ*<
26 9 24 25 syl2an ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y∧A∈X∧L⁡A≤1→M⁡T⁡A≤supx|∃y∈XL⁡y≤1∧x=M⁡T⁡yℝ*<
27 1 2 3 4 5 nmooval ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T=supx|∃y∈XL⁡y≤1∧x=M⁡T⁡yℝ*<
28 27 adantr ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y∧A∈X∧L⁡A≤1→N⁡T=supx|∃y∈XL⁡y≤1∧x=M⁡T⁡yℝ*<
29 26 28 breqtrrd ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y∧A∈X∧L⁡A≤1→M⁡T⁡A≤N⁡T