Metamath Proof Explorer

Theorem nmlnopne0

Description: A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion nmlnopne0 
|- ( T e. LinOp -> ( ( normop ` T ) =/= 0 <-> T =/= 0hop ) )

Proof

Step Hyp Ref Expression
1 nmlnop0 
 |-  ( T e. LinOp -> ( ( normop ` T ) = 0 <-> T = 0hop ) )
2 1 necon3bid 
 |-  ( T e. LinOp -> ( ( normop ` T ) =/= 0 <-> T =/= 0hop ) )