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 ⊢ T : ℋ ⟶ ℋ → 0 ≤ norm op ⁡ T

Proof

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