Metamath Proof Explorer

Theorem nmlnop0

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

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

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( ( normop ` T ) = 0 <-> ( normop ` if ( T e. LinOp , T , 0hop ) ) = 0 ) )
2 eqeq1 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( T = 0hop <-> if ( T e. LinOp , T , 0hop ) = 0hop ) )
3 1 2 bibi12d 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( ( ( normop ` T ) = 0 <-> T = 0hop ) <-> ( ( normop ` if ( T e. LinOp , T , 0hop ) ) = 0 <-> if ( T e. LinOp , T , 0hop ) = 0hop ) ) )
4 0lnop 
 |-  0hop e. LinOp
5 4 elimel 
 |-  if ( T e. LinOp , T , 0hop ) e. LinOp
6 5 nmlnop0iHIL 
 |-  ( ( normop ` if ( T e. LinOp , T , 0hop ) ) = 0 <-> if ( T e. LinOp , T , 0hop ) = 0hop )
7 3 6 dedth 
 |-  ( T e. LinOp -> ( ( normop ` T ) = 0 <-> T = 0hop ) )