Theorem nmlnopgt0i

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
Hypothesis	nmlnop0.1	⊢ 𝑇 ∈ LinOp
Assertion	nmlnopgt0i	⊢ ( 𝑇 ≠ 0hop ↔ 0 < ( normop ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	⊢ 𝑇 ∈ LinOp
2	1	nmlnop0iHIL	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )
3	2	necon3bii	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 𝑇 ≠ 0hop )
4	1	lnopfi	⊢ 𝑇 : ℋ ⟶ ℋ
5		nmopgt0	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) ) )
6	4 5	ax-mp	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) )
7	3 6	bitr3i	⊢ ( 𝑇 ≠ 0hop ↔ 0 < ( normop ‘ 𝑇 ) )