This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmop0

Description: The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmop0 
|- ( normop ` 0hop ) = 0

Proof

Step Hyp Ref Expression
1 ho0f 
 |-  0hop : ~H --> ~H
2 nmopval 
 |-  ( 0hop : ~H --> ~H -> ( normop ` 0hop ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) } , RR* , < ) )
3 1 2 ax-mp 
 |-  ( normop ` 0hop ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) } , RR* , < )
4 ho0val 
 |-  ( y e. ~H -> ( 0hop ` y ) = 0h )
5 4 fveq2d 
 |-  ( y e. ~H -> ( normh ` ( 0hop ` y ) ) = ( normh ` 0h ) )
6 norm0 
 |-  ( normh ` 0h ) = 0
7 5 6 eqtrdi 
 |-  ( y e. ~H -> ( normh ` ( 0hop ` y ) ) = 0 )
8 7 eqeq2d 
 |-  ( y e. ~H -> ( x = ( normh ` ( 0hop ` y ) ) <-> x = 0 ) )
9 8 anbi2d 
 |-  ( y e. ~H -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ x = 0 ) ) )
10 9 rexbiia 
 |-  ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = 0 ) )
11 ax-hv0cl 
 |-  0h e. ~H
12 0le1 
 |-  0 <_ 1
13 fveq2 
 |-  ( y = 0h -> ( normh ` y ) = ( normh ` 0h ) )
14 13 6 eqtrdi 
 |-  ( y = 0h -> ( normh ` y ) = 0 )
15 14 breq1d 
 |-  ( y = 0h -> ( ( normh ` y ) <_ 1 <-> 0 <_ 1 ) )
16 15 rspcev 
 |-  ( ( 0h e. ~H /\ 0 <_ 1 ) -> E. y e. ~H ( normh ` y ) <_ 1 )
17 11 12 16 mp2an 
 |-  E. y e. ~H ( normh ` y ) <_ 1
18 r19.41v 
 |-  ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = 0 ) <-> ( E. y e. ~H ( normh ` y ) <_ 1 /\ x = 0 ) )
19 17 18 mpbiran 
 |-  ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = 0 ) <-> x = 0 )
20 10 19 bitri 
 |-  ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) <-> x = 0 )
21 20 abbii 
 |-  { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) } = { x | x = 0 }
22 df-sn 
 |-  { 0 } = { x | x = 0 }
23 21 22 eqtr4i 
 |-  { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) } = { 0 }
24 23 supeq1i 
 |-  sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( 0hop ` y ) ) ) } , RR* , < ) = sup ( { 0 } , RR* , < )
25 xrltso 
 |-  < Or RR*
26 0xr 
 |-  0 e. RR*
27 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
28 25 26 27 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
29 3 24 28 3eqtri 
 |-  ( normop ` 0hop ) = 0