Metamath Proof Explorer

Theorem nmfnge0

Description: The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnge0 
|- ( T : ~H --> CC -> 0 <_ ( normfn ` T ) )

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 ffvelcdm 
 |-  ( ( T : ~H --> CC /\ 0h e. ~H ) -> ( T ` 0h ) e. CC )
3 1 2 mpan2 
 |-  ( T : ~H --> CC -> ( T ` 0h ) e. CC )
4 3 absge0d 
 |-  ( T : ~H --> CC -> 0 <_ ( abs ` ( T ` 0h ) ) )
5 norm0 
 |-  ( normh ` 0h ) = 0
6 0le1 
 |-  0 <_ 1
7 5 6 eqbrtri 
 |-  ( normh ` 0h ) <_ 1
8 nmfnlb 
 |-  ( ( T : ~H --> CC /\ 0h e. ~H /\ ( normh ` 0h ) <_ 1 ) -> ( abs ` ( T ` 0h ) ) <_ ( normfn ` T ) )
9 1 7 8 mp3an23 
 |-  ( T : ~H --> CC -> ( abs ` ( T ` 0h ) ) <_ ( normfn ` T ) )
10 3 abscld 
 |-  ( T : ~H --> CC -> ( abs ` ( T ` 0h ) ) e. RR )
11 10 rexrd 
 |-  ( T : ~H --> CC -> ( abs ` ( T ` 0h ) ) e. RR* )
12 nmfnxr 
 |-  ( T : ~H --> CC -> ( normfn ` T ) e. RR* )
13 0xr 
 |-  0 e. RR*
14 xrletr 
 |-  ( ( 0 e. RR* /\ ( abs ` ( T ` 0h ) ) e. RR* /\ ( normfn ` T ) e. RR* ) -> ( ( 0 <_ ( abs ` ( T ` 0h ) ) /\ ( abs ` ( T ` 0h ) ) <_ ( normfn ` T ) ) -> 0 <_ ( normfn ` T ) ) )
15 13 14 mp3an1 
 |-  ( ( ( abs ` ( T ` 0h ) ) e. RR* /\ ( normfn ` T ) e. RR* ) -> ( ( 0 <_ ( abs ` ( T ` 0h ) ) /\ ( abs ` ( T ` 0h ) ) <_ ( normfn ` T ) ) -> 0 <_ ( normfn ` T ) ) )
16 11 12 15 syl2anc 
 |-  ( T : ~H --> CC -> ( ( 0 <_ ( abs ` ( T ` 0h ) ) /\ ( abs ` ( T ` 0h ) ) <_ ( normfn ` T ) ) -> 0 <_ ( normfn ` T ) ) )
17 4 9 16 mp2and 
 |-  ( T : ~H --> CC -> 0 <_ ( normfn ` T ) )