Metamath Proof Explorer

Theorem nmoo0

Description: The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoo0.3 
|- N = ( U normOpOLD W )
nmoo0.0 
|- Z = ( U 0op W )
Assertion nmoo0 
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( N ` Z ) = 0 )

Proof

Step Hyp Ref Expression
1 nmoo0.3 
 |-  N = ( U normOpOLD W )
2 nmoo0.0 
 |-  Z = ( U 0op W )
3 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
4 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
5 3 4 2 0oo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z : ( BaseSet ` U ) --> ( BaseSet ` W ) )
6 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
7 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
8 3 4 6 7 1 nmooval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ Z : ( BaseSet ` U ) --> ( BaseSet ` W ) ) -> ( N ` Z ) = sup ( { x | E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) } , RR* , < ) )
9 5 8 mpd3an3 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( N ` Z ) = sup ( { x | E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) } , RR* , < ) )
10 df-sn 
 |-  { 0 } = { x | x = 0 }
11 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
12 3 11 nvzcl 
 |-  ( U e. NrmCVec -> ( 0vec ` U ) e. ( BaseSet ` U ) )
13 11 6 nvz0 
 |-  ( U e. NrmCVec -> ( ( normCV ` U ) ` ( 0vec ` U ) ) = 0 )
14 0le1 
 |-  0 <_ 1
15 13 14 eqbrtrdi 
 |-  ( U e. NrmCVec -> ( ( normCV ` U ) ` ( 0vec ` U ) ) <_ 1 )
16 fveq2 
 |-  ( z = ( 0vec ` U ) -> ( ( normCV ` U ) ` z ) = ( ( normCV ` U ) ` ( 0vec ` U ) ) )
17 16 breq1d 
 |-  ( z = ( 0vec ` U ) -> ( ( ( normCV ` U ) ` z ) <_ 1 <-> ( ( normCV ` U ) ` ( 0vec ` U ) ) <_ 1 ) )
18 17 rspcev 
 |-  ( ( ( 0vec ` U ) e. ( BaseSet ` U ) /\ ( ( normCV ` U ) ` ( 0vec ` U ) ) <_ 1 ) -> E. z e. ( BaseSet ` U ) ( ( normCV ` U ) ` z ) <_ 1 )
19 12 15 18 syl2anc 
 |-  ( U e. NrmCVec -> E. z e. ( BaseSet ` U ) ( ( normCV ` U ) ` z ) <_ 1 )
20 19 biantrurd 
 |-  ( U e. NrmCVec -> ( x = 0 <-> ( E. z e. ( BaseSet ` U ) ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) ) )
21 20 adantr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( x = 0 <-> ( E. z e. ( BaseSet ` U ) ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) ) )
22 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
23 3 22 2 0oval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ z e. ( BaseSet ` U ) ) -> ( Z ` z ) = ( 0vec ` W ) )
24 23 3expa 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ z e. ( BaseSet ` U ) ) -> ( Z ` z ) = ( 0vec ` W ) )
25 24 fveq2d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ z e. ( BaseSet ` U ) ) -> ( ( normCV ` W ) ` ( Z ` z ) ) = ( ( normCV ` W ) ` ( 0vec ` W ) ) )
26 22 7 nvz0 
 |-  ( W e. NrmCVec -> ( ( normCV ` W ) ` ( 0vec ` W ) ) = 0 )
27 26 ad2antlr 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ z e. ( BaseSet ` U ) ) -> ( ( normCV ` W ) ` ( 0vec ` W ) ) = 0 )
28 25 27 eqtrd 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ z e. ( BaseSet ` U ) ) -> ( ( normCV ` W ) ` ( Z ` z ) ) = 0 )
29 28 eqeq2d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ z e. ( BaseSet ` U ) ) -> ( x = ( ( normCV ` W ) ` ( Z ` z ) ) <-> x = 0 ) )
30 29 anbi2d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ z e. ( BaseSet ` U ) ) -> ( ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) <-> ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) ) )
31 30 rexbidva 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) <-> E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) ) )
32 r19.41v 
 |-  ( E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) <-> ( E. z e. ( BaseSet ` U ) ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) )
33 31 32 bitr2di 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( ( E. z e. ( BaseSet ` U ) ( ( normCV ` U ) ` z ) <_ 1 /\ x = 0 ) <-> E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) ) )
34 21 33 bitrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( x = 0 <-> E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) ) )
35 34 abbidv 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> { x | x = 0 } = { x | E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) } )
36 10 35 eqtr2id 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> { x | E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) } = { 0 } )
37 36 supeq1d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> sup ( { x | E. z e. ( BaseSet ` U ) ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( Z ` z ) ) ) } , RR* , < ) = sup ( { 0 } , RR* , < ) )
38 9 37 eqtrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( N ` Z ) = sup ( { 0 } , RR* , < ) )
39 xrltso 
 |-  < Or RR*
40 0xr 
 |-  0 e. RR*
41 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
42 39 40 41 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
43 38 42 eqtrdi 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( N ` Z ) = 0 )