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 ‘ 𝑇 ) )