Metamath Proof Explorer

Theorem nmooge0

Description: The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 
|- X = ( BaseSet ` U )
nmoxr.2 
|- Y = ( BaseSet ` W )
nmoxr.3 
|- N = ( U normOpOLD W )
Assertion nmooge0 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 <_ ( N ` T ) )

Proof

Step Hyp Ref Expression
1 nmoxr.1 
 |-  X = ( BaseSet ` U )
2 nmoxr.2 
 |-  Y = ( BaseSet ` W )
3 nmoxr.3 
 |-  N = ( U normOpOLD W )
4 0xr 
 |-  0 e. RR*
5 4 a1i 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 e. RR* )
6 simp2 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> W e. NrmCVec )
7 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
8 1 7 nvzcl 
 |-  ( U e. NrmCVec -> ( 0vec ` U ) e. X )
9 ffvelrn 
 |-  ( ( T : X --> Y /\ ( 0vec ` U ) e. X ) -> ( T ` ( 0vec ` U ) ) e. Y )
10 8 9 sylan2 
 |-  ( ( T : X --> Y /\ U e. NrmCVec ) -> ( T ` ( 0vec ` U ) ) e. Y )
11 10 ancoms 
 |-  ( ( U e. NrmCVec /\ T : X --> Y ) -> ( T ` ( 0vec ` U ) ) e. Y )
12 11 3adant2 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( T ` ( 0vec ` U ) ) e. Y )
13 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
14 2 13 nvcl 
 |-  ( ( W e. NrmCVec /\ ( T ` ( 0vec ` U ) ) e. Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. RR )
15 6 12 14 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. RR )
16 15 rexrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. RR* )
17 1 2 3 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* )
18 2 13 nvge0 
 |-  ( ( W e. NrmCVec /\ ( T ` ( 0vec ` U ) ) e. Y ) -> 0 <_ ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) )
19 6 12 18 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 <_ ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) )
20 2 13 nmosetre 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR )
21 ressxr 
 |-  RR C_ RR*
22 20 21 sstrdi 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR* )
23 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
24 1 7 23 nmosetn0 
 |-  ( U e. NrmCVec -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } )
25 supxrub 
 |-  ( ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR* /\ ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) )
26 22 24 25 syl2an 
 |-  ( ( ( W e. NrmCVec /\ T : X --> Y ) /\ U e. NrmCVec ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) )
27 26 3impa 
 |-  ( ( W e. NrmCVec /\ T : X --> Y /\ U e. NrmCVec ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) )
28 27 3comr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) )
29 1 2 23 13 3 nmooval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) )
30 28 29 breqtrrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ ( N ` T ) )
31 5 16 17 19 30 xrletrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 <_ ( N ` T ) )