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 : ~H --> ~H -> ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmopxr	|- ( T : ~H --> ~H -> ( normop ` T ) e. RR* )
2		nmopge0	|- ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )
3		0xr	|- 0 e. RR*
4		xrleltne	|- ( ( 0 e. RR* /\ ( normop ` T ) e. RR* /\ 0 <_ ( normop ` T ) ) -> ( 0 < ( normop ` T ) <-> ( normop ` T ) =/= 0 ) )
5	3 4	mp3an1	|- ( ( ( normop ` T ) e. RR* /\ 0 <_ ( normop ` T ) ) -> ( 0 < ( normop ` T ) <-> ( normop ` T ) =/= 0 ) )
6	1 2 5	syl2anc	|- ( T : ~H --> ~H -> ( 0 < ( normop ` T ) <-> ( normop ` T ) =/= 0 ) )
7	6	bicomd	|- ( T : ~H --> ~H -> ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) ) )