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 ≤ norm op ⁡ 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 ≤ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
22 4 20 21 syl2anc ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ T ⁡ A ≤ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
23 nmopval ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
24 23 3ad2ant1 ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
25 22 24 breqtrrd ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T