Theorem nmlno0i

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmlno0.3	|- N = ( U normOpOLD W )
	nmlno0.0	|- Z = ( U 0op W )
	nmlno0.7	|- L = ( U LnOp W )
	nmlno0i.u	|- U e. NrmCVec
	nmlno0i.w	|- W e. NrmCVec
Assertion	nmlno0i	|- ( T e. L -> ( ( N ` T ) = 0 <-> T = Z ) )

Proof

Step	Hyp	Ref	Expression
1		nmlno0.3	|- N = ( U normOpOLD W )
2		nmlno0.0	|- Z = ( U 0op W )
3		nmlno0.7	|- L = ( U LnOp W )
4		nmlno0i.u	|- U e. NrmCVec
5		nmlno0i.w	|- W e. NrmCVec
6		fveqeq2	|- ( T = if ( T e. L , T , Z ) -> ( ( N ` T ) = 0 <-> ( N ` if ( T e. L , T , Z ) ) = 0 ) )
7		eqeq1	|- ( T = if ( T e. L , T , Z ) -> ( T = Z <-> if ( T e. L , T , Z ) = Z ) )
8	6 7	bibi12d	|- ( T = if ( T e. L , T , Z ) -> ( ( ( N ` T ) = 0 <-> T = Z ) <-> ( ( N ` if ( T e. L , T , Z ) ) = 0 <-> if ( T e. L , T , Z ) = Z ) ) )
9	2 3	0lno	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z e. L )
10	4 5 9	mp2an	|- Z e. L
11	10	elimel	|- if ( T e. L , T , Z ) e. L
12		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
13		eqid	|- ( BaseSet ` W ) = ( BaseSet ` W )
14		eqid	|- ( .sOLD ` U ) = ( .sOLD ` U )
15		eqid	|- ( .sOLD ` W ) = ( .sOLD ` W )
16		eqid	|- ( 0vec ` U ) = ( 0vec ` U )
17		eqid	|- ( 0vec ` W ) = ( 0vec ` W )
18		eqid	|- ( normCV ` U ) = ( normCV ` U )
19		eqid	|- ( normCV ` W ) = ( normCV ` W )
20	1 2 3 4 5 11 12 13 14 15 16 17 18 19	nmlno0lem	|- ( ( N ` if ( T e. L , T , Z ) ) = 0 <-> if ( T e. L , T , Z ) = Z )
21	8 20	dedth	|- ( T e. L -> ( ( N ` T ) = 0 <-> T = Z ) )