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 ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ( norm ‘ ( 𝑇𝐴 ) ) ≤ ( normop𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmopsetretHIL ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ⊆ ℝ )
2 ressxr ℝ ⊆ ℝ*
3 1 2 sstrdi ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ⊆ ℝ* )
4 3 3ad2ant1 ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ⊆ ℝ* )
5 fveq2 ( 𝑦 = 𝐴 → ( norm𝑦 ) = ( norm𝐴 ) )
6 5 breq1d ( 𝑦 = 𝐴 → ( ( norm𝑦 ) ≤ 1 ↔ ( norm𝐴 ) ≤ 1 ) )
7 2fveq3 ( 𝑦 = 𝐴 → ( norm ‘ ( 𝑇𝑦 ) ) = ( norm ‘ ( 𝑇𝐴 ) ) )
8 7 eqeq2d ( 𝑦 = 𝐴 → ( ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ↔ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝐴 ) ) ) )
9 6 8 anbi12d ( 𝑦 = 𝐴 → ( ( ( norm𝑦 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) ↔ ( ( norm𝐴 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝐴 ) ) ) ) )
10 eqid ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝐴 ) )
11 10 biantru ( ( norm𝐴 ) ≤ 1 ↔ ( ( norm𝐴 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝐴 ) ) ) )
12 9 11 bitr4di ( 𝑦 = 𝐴 → ( ( ( norm𝑦 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) ↔ ( norm𝐴 ) ≤ 1 ) )
13 12 rspcev ( ( 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) )
14 fvex ( norm ‘ ( 𝑇𝐴 ) ) ∈ V
15 eqeq1 ( 𝑥 = ( norm ‘ ( 𝑇𝐴 ) ) → ( 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ↔ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) )
16 15 anbi2d ( 𝑥 = ( norm ‘ ( 𝑇𝐴 ) ) → ( ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) ↔ ( ( norm𝑦 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) ) )
17 16 rexbidv ( 𝑥 = ( norm ‘ ( 𝑇𝐴 ) ) → ( ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) ) )
18 14 17 elab ( ( norm ‘ ( 𝑇𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ↔ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ ( norm ‘ ( 𝑇𝐴 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) ) )
19 13 18 sylibr ( ( 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ( norm ‘ ( 𝑇𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } )
20 19 3adant1 ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ( norm ‘ ( 𝑇𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } )
21 supxrub ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ⊆ ℝ* ∧ ( norm ‘ ( 𝑇𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ) → ( norm ‘ ( 𝑇𝐴 ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )
22 4 20 21 syl2anc ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ( norm ‘ ( 𝑇𝐴 ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )
23 nmopval ( 𝑇 : ℋ ⟶ ℋ → ( normop𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )
24 23 3ad2ant1 ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ( normop𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )
25 22 24 breqtrrd ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ ( norm𝐴 ) ≤ 1 ) → ( norm ‘ ( 𝑇𝐴 ) ) ≤ ( normop𝑇 ) )