Theorem nmopge0

Description: The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopge0	⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 0ℎ ∈ ℋ ) → ( 𝑇 ‘ 0ℎ ) ∈ ℋ )
3	1 2	mpan2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ‘ 0ℎ ) ∈ ℋ )
4		normge0	⊢ ( ( 𝑇 ‘ 0ℎ ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) )
5	3 4	syl	⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) )
6		norm0	⊢ ( normℎ ‘ 0ℎ ) = 0
7		0le1	⊢ 0 ≤ 1
8	6 7	eqbrtri	⊢ ( normℎ ‘ 0ℎ ) ≤ 1
9		nmoplb	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 0ℎ ∈ ℋ ∧ ( normℎ ‘ 0ℎ ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( normop ‘ 𝑇 ) )
10	1 8 9	mp3an23	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( normop ‘ 𝑇 ) )
11		normcl	⊢ ( ( 𝑇 ‘ 0ℎ ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ ℝ )
12	3 11	syl	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ ℝ )
13	12	rexrd	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ ℝ* )
14		nmopxr	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* )
15		0xr	⊢ 0 ∈ ℝ*
16		xrletr	⊢ ( ( 0 ∈ ℝ* ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ ℝ* ∧ ( normop ‘ 𝑇 ) ∈ ℝ* ) → ( ( 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( normop ‘ 𝑇 ) ) → 0 ≤ ( normop ‘ 𝑇 ) ) )
17	15 16	mp3an1	⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ ℝ* ∧ ( normop ‘ 𝑇 ) ∈ ℝ* ) → ( ( 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( normop ‘ 𝑇 ) ) → 0 ≤ ( normop ‘ 𝑇 ) ) )
18	13 14 17	syl2anc	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( normop ‘ 𝑇 ) ) → 0 ≤ ( normop ‘ 𝑇 ) ) )
19	5 10 18	mp2and	⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ 𝑇 ) )