Metamath Proof Explorer

Theorem nmoplb

Description: A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmoplb ⊢T:ℋ⟶ℋ∧A∈ℋ∧normℎ⁡A≤1→normℎ⁡T⁡A≤normop⁡T

Proof

Step Hyp Ref Expression
1 nmopsetretHIL ⊢T:ℋ⟶ℋ→x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y⊆ℝ
2 ressxr ⊢ℝ⊆ℝ*
3 1 2 sstrdi ⊢T:ℋ⟶ℋ→x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y⊆ℝ*
4 3 3ad2ant1 ⊢T:ℋ⟶ℋ∧A∈ℋ∧normℎ⁡A≤1→x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y⊆ℝ*
5 fveq2 ⊢y=A→normℎ⁡y=normℎ⁡A
6 5 breq1d ⊢y=A→normℎ⁡y≤1↔normℎ⁡A≤1
7 2fveq3 ⊢y=A→normℎ⁡T⁡y=normℎ⁡T⁡A
8 7 eqeq2d ⊢y=A→normℎ⁡T⁡A=normℎ⁡T⁡y↔normℎ⁡T⁡A=normℎ⁡T⁡A
9 6 8 anbi12d ⊢y=A→normℎ⁡y≤1∧normℎ⁡T⁡A=normℎ⁡T⁡y↔normℎ⁡A≤1∧normℎ⁡T⁡A=normℎ⁡T⁡A
10 eqid ⊢normℎ⁡T⁡A=normℎ⁡T⁡A
11 10 biantru ⊢normℎ⁡A≤1↔normℎ⁡A≤1∧normℎ⁡T⁡A=normℎ⁡T⁡A
12 9 11 bitr4di ⊢y=A→normℎ⁡y≤1∧normℎ⁡T⁡A=normℎ⁡T⁡y↔normℎ⁡A≤1
13 12 rspcev ⊢A∈ℋ∧normℎ⁡A≤1→∃y∈ℋnormℎ⁡y≤1∧normℎ⁡T⁡A=normℎ⁡T⁡y
14 fvex ⊢normℎ⁡T⁡A∈V
15 eqeq1 ⊢x=normℎ⁡T⁡A→x=normℎ⁡T⁡y↔normℎ⁡T⁡A=normℎ⁡T⁡y
16 15 anbi2d ⊢x=normℎ⁡T⁡A→normℎ⁡y≤1∧x=normℎ⁡T⁡y↔normℎ⁡y≤1∧normℎ⁡T⁡A=normℎ⁡T⁡y
17 16 rexbidv ⊢x=normℎ⁡T⁡A→∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y↔∃y∈ℋnormℎ⁡y≤1∧normℎ⁡T⁡A=normℎ⁡T⁡y
18 14 17 elab ⊢normℎ⁡T⁡A∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y↔∃y∈ℋnormℎ⁡y≤1∧normℎ⁡T⁡A=normℎ⁡T⁡y
19 13 18 sylibr ⊢A∈ℋ∧normℎ⁡A≤1→normℎ⁡T⁡A∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y
20 19 3adant1 ⊢T:ℋ⟶ℋ∧A∈ℋ∧normℎ⁡A≤1→normℎ⁡T⁡A∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y
21 supxrub ⊢x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y⊆ℝ*∧normℎ⁡T⁡A∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y→normℎ⁡T⁡A≤supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
22 4 20 21 syl2anc ⊢T:ℋ⟶ℋ∧A∈ℋ∧normℎ⁡A≤1→normℎ⁡T⁡A≤supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
23 nmopval ⊢T:ℋ⟶ℋ→normop⁡T=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
24 23 3ad2ant1 ⊢T:ℋ⟶ℋ∧A∈ℋ∧normℎ⁡A≤1→normop⁡T=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
25 22 24 breqtrrd ⊢T:ℋ⟶ℋ∧A∈ℋ∧normℎ⁡A≤1→normℎ⁡T⁡A≤normop⁡T