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 syl6rbb
 |-  ( ( 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 syl5req
 |-  ( ( 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 )