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 ‘ 𝑇 ) )