Metamath Proof Explorer

Theorem nmfnge0

Description: The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnge0 ⊢ T : ℋ ⟶ ℂ → 0 ≤ norm fn ⁡ T

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
2 ffvelrn ⊢ T : ℋ ⟶ ℂ ∧ 0 ℎ ∈ ℋ → T ⁡ 0 ℎ ∈ ℂ
3 1 2 mpan2 ⊢ T : ℋ ⟶ ℂ → T ⁡ 0 ℎ ∈ ℂ
4 3 absge0d ⊢ T : ℋ ⟶ ℂ → 0 ≤ T ⁡ 0 ℎ
5 norm0 ⊢ norm ℎ ⁡ 0 ℎ = 0
6 0le1 ⊢ 0 ≤ 1
7 5 6 eqbrtri ⊢ norm ℎ ⁡ 0 ℎ ≤ 1
8 nmfnlb ⊢ T : ℋ ⟶ ℂ ∧ 0 ℎ ∈ ℋ ∧ norm ℎ ⁡ 0 ℎ ≤ 1 → T ⁡ 0 ℎ ≤ norm fn ⁡ T
9 1 7 8 mp3an23 ⊢ T : ℋ ⟶ ℂ → T ⁡ 0 ℎ ≤ norm fn ⁡ T
10 3 abscld ⊢ T : ℋ ⟶ ℂ → T ⁡ 0 ℎ ∈ ℝ
11 10 rexrd ⊢ T : ℋ ⟶ ℂ → T ⁡ 0 ℎ ∈ ℝ *
12 nmfnxr ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T ∈ ℝ *
13 0xr ⊢ 0 ∈ ℝ *
14 xrletr ⊢ 0 ∈ ℝ * ∧ T ⁡ 0 ℎ ∈ ℝ * ∧ norm fn ⁡ T ∈ ℝ * → 0 ≤ T ⁡ 0 ℎ ∧ T ⁡ 0 ℎ ≤ norm fn ⁡ T → 0 ≤ norm fn ⁡ T
15 13 14 mp3an1 ⊢ T ⁡ 0 ℎ ∈ ℝ * ∧ norm fn ⁡ T ∈ ℝ * → 0 ≤ T ⁡ 0 ℎ ∧ T ⁡ 0 ℎ ≤ norm fn ⁡ T → 0 ≤ norm fn ⁡ T
16 11 12 15 syl2anc ⊢ T : ℋ ⟶ ℂ → 0 ≤ T ⁡ 0 ℎ ∧ T ⁡ 0 ℎ ≤ norm fn ⁡ T → 0 ≤ norm fn ⁡ T
17 4 9 16 mp2and ⊢ T : ℋ ⟶ ℂ → 0 ≤ norm fn ⁡ T