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	|- T e. LinOp
Assertion	nmlnopgt0i	|- ( T =/= 0hop <-> 0 < ( normop ` T ) )

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	|- T e. LinOp
2	1	nmlnop0iHIL	|- ( ( normop ` T ) = 0 <-> T = 0hop )
3	2	necon3bii	|- ( ( normop ` T ) =/= 0 <-> T =/= 0hop )
4	1	lnopfi	|- T : ~H --> ~H
5		nmopgt0	|- ( T : ~H --> ~H -> ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) ) )
6	4 5	ax-mp	|- ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) )
7	3 6	bitr3i	|- ( T =/= 0hop <-> 0 < ( normop ` T ) )