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

Metamath Proof Explorer

Theorem nmopgt0

Description: A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopgt0 ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T ≠ 0 ↔ 0 < norm op ⁡ T

Proof

Step Hyp Ref Expression
1 nmopxr ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T ∈ ℝ *
2 nmopge0 ⊢ T : ℋ ⟶ ℋ → 0 ≤ norm op ⁡ T
3 0xr ⊢ 0 ∈ ℝ *
4 xrleltne ⊢ 0 ∈ ℝ * ∧ norm op ⁡ T ∈ ℝ * ∧ 0 ≤ norm op ⁡ T → 0 < norm op ⁡ T ↔ norm op ⁡ T ≠ 0
5 3 4 mp3an1 ⊢ norm op ⁡ T ∈ ℝ * ∧ 0 ≤ norm op ⁡ T → 0 < norm op ⁡ T ↔ norm op ⁡ T ≠ 0
6 1 2 5 syl2anc ⊢ T : ℋ ⟶ ℋ → 0 < norm op ⁡ T ↔ norm op ⁡ T ≠ 0
7 6 bicomd ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T ≠ 0 ↔ 0 < norm op ⁡ T