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 )