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

Metamath Proof Explorer

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 ) )