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

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 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 ‘ 𝑇 ) )