Metamath Proof Explorer

Theorem nmfnlb

Description: A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnlb ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → T ⁡ A ≤ norm fn ⁡ T

Proof

Step Hyp Ref Expression
1 nmfnsetre ⊢ T : ℋ ⟶ ℂ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ
2 ressxr ⊢ ℝ ⊆ ℝ *
3 1 2 sstrdi ⊢ T : ℋ ⟶ ℂ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ *
4 3 3ad2ant1 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = 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 → T ⁡ y = T ⁡ A
8 7 eqeq2d ⊢ y = A → T ⁡ A = T ⁡ y ↔ T ⁡ A = T ⁡ A
9 6 8 anbi12d ⊢ y = A → norm ℎ ⁡ y ≤ 1 ∧ T ⁡ A = T ⁡ y ↔ norm ℎ ⁡ A ≤ 1 ∧ T ⁡ A = T ⁡ A
10 eqid ⊢ T ⁡ A = T ⁡ A
11 10 biantru ⊢ norm ℎ ⁡ A ≤ 1 ↔ norm ℎ ⁡ A ≤ 1 ∧ T ⁡ A = T ⁡ A
12 9 11 bitr4di ⊢ y = A → norm ℎ ⁡ y ≤ 1 ∧ T ⁡ A = T ⁡ y ↔ norm ℎ ⁡ A ≤ 1
13 12 rspcev ⊢ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ A = T ⁡ y
14 fvex ⊢ T ⁡ A ∈ V
15 eqeq1 ⊢ x = T ⁡ A → x = T ⁡ y ↔ T ⁡ A = T ⁡ y
16 15 anbi2d ⊢ x = T ⁡ A → norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ A = T ⁡ y
17 16 rexbidv ⊢ x = T ⁡ A → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ A = T ⁡ y
18 14 17 elab ⊢ T ⁡ A ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ A = T ⁡ y
19 13 18 sylibr ⊢ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → T ⁡ A ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y
20 19 3adant1 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → T ⁡ A ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y
21 supxrub ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ * ∧ T ⁡ A ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y → T ⁡ A ≤ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
22 4 20 21 syl2anc ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → T ⁡ A ≤ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
23 nmfnval ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
24 23 3ad2ant1 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm fn ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
25 22 24 breqtrrd ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → T ⁡ A ≤ norm fn ⁡ T