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 ‘ 𝑇 ) ) )