Metamath Proof Explorer

Theorem nmlnogt0

Description: The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmlnogt0.3 
|- N = ( U normOpOLD W )
nmlnogt0.0 
|- Z = ( U 0op W )
nmlnogt0.7 
|- L = ( U LnOp W )
Assertion nmlnogt0 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T =/= Z <-> 0 < ( N ` T ) ) )

Proof

Step Hyp Ref Expression
1 nmlnogt0.3 
 |-  N = ( U normOpOLD W )
2 nmlnogt0.0 
 |-  Z = ( U 0op W )
3 nmlnogt0.7 
 |-  L = ( U LnOp W )
4 1 2 3 nmlno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( N ` T ) = 0 <-> T = Z ) )
5 4 necon3bid 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( N ` T ) =/= 0 <-> T =/= Z ) )
6 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
7 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
8 6 7 3 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : ( BaseSet ` U ) --> ( BaseSet ` W ) )
9 6 7 1 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : ( BaseSet ` U ) --> ( BaseSet ` W ) ) -> ( N ` T ) e. RR* )
10 6 7 1 nmooge0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : ( BaseSet ` U ) --> ( BaseSet ` W ) ) -> 0 <_ ( N ` T ) )
11 0xr 
 |-  0 e. RR*
12 xrlttri2 
 |-  ( ( ( N ` T ) e. RR* /\ 0 e. RR* ) -> ( ( N ` T ) =/= 0 <-> ( ( N ` T ) < 0 \/ 0 < ( N ` T ) ) ) )
13 11 12 mpan2 
 |-  ( ( N ` T ) e. RR* -> ( ( N ` T ) =/= 0 <-> ( ( N ` T ) < 0 \/ 0 < ( N ` T ) ) ) )
14 13 adantr 
 |-  ( ( ( N ` T ) e. RR* /\ 0 <_ ( N ` T ) ) -> ( ( N ` T ) =/= 0 <-> ( ( N ` T ) < 0 \/ 0 < ( N ` T ) ) ) )
15 xrlenlt 
 |-  ( ( 0 e. RR* /\ ( N ` T ) e. RR* ) -> ( 0 <_ ( N ` T ) <-> -. ( N ` T ) < 0 ) )
16 11 15 mpan 
 |-  ( ( N ` T ) e. RR* -> ( 0 <_ ( N ` T ) <-> -. ( N ` T ) < 0 ) )
17 16 biimpa 
 |-  ( ( ( N ` T ) e. RR* /\ 0 <_ ( N ` T ) ) -> -. ( N ` T ) < 0 )
18 biorf 
 |-  ( -. ( N ` T ) < 0 -> ( 0 < ( N ` T ) <-> ( ( N ` T ) < 0 \/ 0 < ( N ` T ) ) ) )
19 17 18 syl 
 |-  ( ( ( N ` T ) e. RR* /\ 0 <_ ( N ` T ) ) -> ( 0 < ( N ` T ) <-> ( ( N ` T ) < 0 \/ 0 < ( N ` T ) ) ) )
20 14 19 bitr4d 
 |-  ( ( ( N ` T ) e. RR* /\ 0 <_ ( N ` T ) ) -> ( ( N ` T ) =/= 0 <-> 0 < ( N ` T ) ) )
21 9 10 20 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : ( BaseSet ` U ) --> ( BaseSet ` W ) ) -> ( ( N ` T ) =/= 0 <-> 0 < ( N ` T ) ) )
22 8 21 syld3an3 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( N ` T ) =/= 0 <-> 0 < ( N ` T ) ) )
23 5 22 bitr3d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T =/= Z <-> 0 < ( N ` T ) ) )