# 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`