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

Metamath Proof Explorer

Theorem nmfn0

Description: The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfn0 
|- ( normfn ` ( ~H X. { 0 } ) ) = 0

Proof

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