Metamath Proof Explorer

Theorem nmcfnlb

Description: A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elin ⊢ T ∈ LinFn ∩ ContFn ↔ T ∈ LinFn ∧ T ∈ ContFn
2 fveq1 ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ A = if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ A
3 2 fveq2d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ A = if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ A
4 fveq2 ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → norm fn ⁡ T = norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0
5 4 oveq1d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → norm fn ⁡ T ⁢ norm ℎ ⁡ A = norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁢ norm ℎ ⁡ A
6 3 5 breq12d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A ↔ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ A ≤ norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁢ norm ℎ ⁡ A
7 6 imbi2d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A ↔ A ∈ ℋ → if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ A ≤ norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁢ norm ℎ ⁡ A
8 0lnfn ⊢ ℋ × 0 ∈ LinFn
9 0cnfn ⊢ ℋ × 0 ∈ ContFn
10 elin ⊢ ℋ × 0 ∈ LinFn ∩ ContFn ↔ ℋ × 0 ∈ LinFn ∧ ℋ × 0 ∈ ContFn
11 8 9 10 mpbir2an ⊢ ℋ × 0 ∈ LinFn ∩ ContFn
12 11 elimel ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∩ ContFn
13 elin ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∩ ContFn ↔ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∧ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
14 12 13 mpbi ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∧ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
15 14 simpli ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn
16 14 simpri ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
17 15 16 nmcfnlbi ⊢ A ∈ ℋ → if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ A ≤ norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁢ norm ℎ ⁡ A
18 7 17 dedth ⊢ T ∈ LinFn ∩ ContFn → A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A
19 18 imp ⊢ T ∈ LinFn ∩ ContFn ∧ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A
20 1 19 sylanbr ⊢ T ∈ LinFn ∧ T ∈ ContFn ∧ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A
21 20 3impa ⊢ T ∈ LinFn ∧ T ∈ ContFn ∧ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A