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≤normfn⁡T

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢0ℎ∈ℋ
2 ffvelcdm ⊢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ℎ≤normfn⁡T
9 1 7 8 mp3an23 ⊢T:ℋ⟶ℂ→T⁡0ℎ≤normfn⁡T
10 3 abscld ⊢T:ℋ⟶ℂ→T⁡0ℎ∈ℝ
11 10 rexrd ⊢T:ℋ⟶ℂ→T⁡0ℎ∈ℝ*
12 nmfnxr ⊢T:ℋ⟶ℂ→normfn⁡T∈ℝ*
13 0xr ⊢0∈ℝ*
14 xrletr ⊢0∈ℝ*∧T⁡0ℎ∈ℝ*∧normfn⁡T∈ℝ*→0≤T⁡0ℎ∧T⁡0ℎ≤normfn⁡T→0≤normfn⁡T
15 13 14 mp3an1 ⊢T⁡0ℎ∈ℝ*∧normfn⁡T∈ℝ*→0≤T⁡0ℎ∧T⁡0ℎ≤normfn⁡T→0≤normfn⁡T
16 11 12 15 syl2anc ⊢T:ℋ⟶ℂ→0≤T⁡0ℎ∧T⁡0ℎ≤normfn⁡T→0≤normfn⁡T
17 4 9 16 mp2and ⊢T:ℋ⟶ℂ→0≤normfn⁡T