This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmlnop0iHIL

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nmlnop0.1 
 |-  T e. LinOp
2 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
3 eqid 
 |-  ( <. <. +h , .h >. , normh >. normOpOLD <. <. +h , .h >. , normh >. ) = ( <. <. +h , .h >. , normh >. normOpOLD <. <. +h , .h >. , normh >. )
4 2 3 hhnmoi 
 |-  normop = ( <. <. +h , .h >. , normh >. normOpOLD <. <. +h , .h >. , normh >. )
5 eqid 
 |-  ( <. <. +h , .h >. , normh >. 0op <. <. +h , .h >. , normh >. ) = ( <. <. +h , .h >. , normh >. 0op <. <. +h , .h >. , normh >. )
6 2 5 hh0oi 
 |-  0hop = ( <. <. +h , .h >. , normh >. 0op <. <. +h , .h >. , normh >. )
7 eqid 
 |-  ( <. <. +h , .h >. , normh >. LnOp <. <. +h , .h >. , normh >. ) = ( <. <. +h , .h >. , normh >. LnOp <. <. +h , .h >. , normh >. )
8 2 7 hhlnoi 
 |-  LinOp = ( <. <. +h , .h >. , normh >. LnOp <. <. +h , .h >. , normh >. )
9 2 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
10 4 6 8 9 9 nmlno0i 
 |-  ( T e. LinOp -> ( ( normop ` T ) = 0 <-> T = 0hop ) )
11 1 10 ax-mp 
 |-  ( ( normop ` T ) = 0 <-> T = 0hop )