This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑇 : ℋ ⟶ ℂ → 0 ≤ ( normfn ‘ 𝑇 ) )

Proof

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