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 ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 nmopxr ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* )
2 nmopge0 ⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ 𝑇 ) )
3 0xr ⊢ 0 ∈ ℝ*
4 xrleltne ⊢ ( ( 0 ∈ ℝ* ∧ ( normop ‘ 𝑇 ) ∈ ℝ* ∧ 0 ≤ ( normop ‘ 𝑇 ) ) → ( 0 < ( normop ‘ 𝑇 ) ↔ ( normop ‘ 𝑇 ) ≠ 0 ) )
5 3 4 mp3an1 ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ* ∧ 0 ≤ ( normop ‘ 𝑇 ) ) → ( 0 < ( normop ‘ 𝑇 ) ↔ ( normop ‘ 𝑇 ) ≠ 0 ) )
6 1 2 5 syl2anc ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 0 < ( normop ‘ 𝑇 ) ↔ ( normop ‘ 𝑇 ) ≠ 0 ) )
7 6 bicomd ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) ) )