# 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$