Metamath Proof Explorer

Theorem nmlno0

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-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 )
Assertion nmlno0 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ 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 oveq1 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( U LnOp W ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) )
5 3 4 eqtrid 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> L = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) )
6 5 eleq2d 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( T e. L <-> T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) ) )
7 oveq1 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( U normOpOLD W ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) )
8 1 7 eqtrid 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> N = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) )
9 8 fveq1d 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( N ` T ) = ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) )
10 9 eqeq1d 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( ( N ` T ) = 0 <-> ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = 0 ) )
11 oveq1 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( U 0op W ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) )
12 2 11 eqtrid 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> Z = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) )
13 12 eqeq2d 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( T = Z <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) ) )
14 10 13 bibi12d 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( ( ( N ` T ) = 0 <-> T = Z ) <-> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) ) ) )
15 6 14 imbi12d 
 |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( ( T e. L -> ( ( N ` T ) = 0 <-> T = Z ) ) <-> ( T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) -> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) ) ) ) )
16 oveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
17 16 eleq2d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) <-> T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) )
18 oveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
19 18 fveq1d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` T ) )
20 19 eqeq1d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = 0 <-> ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` T ) = 0 ) )
21 oveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
22 21 eqeq2d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) )
23 20 22 bibi12d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) ) <-> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) ) )
24 17 23 imbi12d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp W ) -> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op W ) ) ) <-> ( T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) -> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) ) ) )
25 eqid 
 |-  ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) )
26 eqid 
 |-  ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) )
27 eqid 
 |-  ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) )
28 elimnvu 
 |-  if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) e. NrmCVec
29 elimnvu 
 |-  if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) e. NrmCVec
30 25 26 27 28 29 nmlno0i 
 |-  ( T e. ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) LnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) -> ( ( ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` T ) = 0 <-> T = ( if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) 0op if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) )
31 15 24 30 dedth2h 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. L -> ( ( N ` T ) = 0 <-> T = Z ) ) )
32 31 3impia 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( N ` T ) = 0 <-> T = Z ) )