Metamath Proof Explorer

Theorem nmbdfnlb

Description: A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion nmbdfnlb ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ ∧ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → T ⁡ A = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁡ A
2 1 fveq2d ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → T ⁡ A = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁡ A
3 fveq2 ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → norm fn ⁡ T = norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0
4 3 oveq1d ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → norm fn ⁡ T ⁢ norm ℎ ⁡ A = norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁢ norm ℎ ⁡ A
5 2 4 breq12d ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A ↔ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁡ A ≤ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁢ norm ℎ ⁡ A
6 5 imbi2d ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A ↔ A ∈ ℋ → if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁡ A ≤ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁢ norm ℎ ⁡ A
7 eleq1 ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → T ∈ LinFn ↔ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ LinFn
8 3 eleq1d ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → norm fn ⁡ T ∈ ℝ ↔ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ ℝ
9 7 8 anbi12d ⊢ T = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ ↔ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ LinFn ∧ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ ℝ
10 eleq1 ⊢ ℋ × 0 = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → ℋ × 0 ∈ LinFn ↔ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ LinFn
11 fveq2 ⊢ ℋ × 0 = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → norm fn ⁡ ℋ × 0 = norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0
12 11 eleq1d ⊢ ℋ × 0 = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → norm fn ⁡ ℋ × 0 ∈ ℝ ↔ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ ℝ
13 10 12 anbi12d ⊢ ℋ × 0 = if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 → ℋ × 0 ∈ LinFn ∧ norm fn ⁡ ℋ × 0 ∈ ℝ ↔ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ LinFn ∧ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ ℝ
14 0lnfn ⊢ ℋ × 0 ∈ LinFn
15 nmfn0 ⊢ norm fn ⁡ ℋ × 0 = 0
16 0re ⊢ 0 ∈ ℝ
17 15 16 eqeltri ⊢ norm fn ⁡ ℋ × 0 ∈ ℝ
18 14 17 pm3.2i ⊢ ℋ × 0 ∈ LinFn ∧ norm fn ⁡ ℋ × 0 ∈ ℝ
19 9 13 18 elimhyp ⊢ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ LinFn ∧ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ∈ ℝ
20 19 nmbdfnlbi ⊢ A ∈ ℋ → if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁡ A ≤ norm fn ⁡ if T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ T ℋ × 0 ⁢ norm ℎ ⁡ A
21 6 20 dedth ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ → A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A
22 21 3impia ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ ∧ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A