Metamath Proof Explorer

Theorem nmopge0

Description: The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopge0 
|- ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ 0h e. ~H ) -> ( T ` 0h ) e. ~H )
3 1 2 mpan2 
 |-  ( T : ~H --> ~H -> ( T ` 0h ) e. ~H )
4 normge0 
 |-  ( ( T ` 0h ) e. ~H -> 0 <_ ( normh ` ( T ` 0h ) ) )
5 3 4 syl 
 |-  ( T : ~H --> ~H -> 0 <_ ( normh ` ( T ` 0h ) ) )
6 norm0 
 |-  ( normh ` 0h ) = 0
7 0le1 
 |-  0 <_ 1
8 6 7 eqbrtri 
 |-  ( normh ` 0h ) <_ 1
9 nmoplb 
 |-  ( ( T : ~H --> ~H /\ 0h e. ~H /\ ( normh ` 0h ) <_ 1 ) -> ( normh ` ( T ` 0h ) ) <_ ( normop ` T ) )
10 1 8 9 mp3an23 
 |-  ( T : ~H --> ~H -> ( normh ` ( T ` 0h ) ) <_ ( normop ` T ) )
11 normcl 
 |-  ( ( T ` 0h ) e. ~H -> ( normh ` ( T ` 0h ) ) e. RR )
12 3 11 syl 
 |-  ( T : ~H --> ~H -> ( normh ` ( T ` 0h ) ) e. RR )
13 12 rexrd 
 |-  ( T : ~H --> ~H -> ( normh ` ( T ` 0h ) ) e. RR* )
14 nmopxr 
 |-  ( T : ~H --> ~H -> ( normop ` T ) e. RR* )
15 0xr 
 |-  0 e. RR*
16 xrletr 
 |-  ( ( 0 e. RR* /\ ( normh ` ( T ` 0h ) ) e. RR* /\ ( normop ` T ) e. RR* ) -> ( ( 0 <_ ( normh ` ( T ` 0h ) ) /\ ( normh ` ( T ` 0h ) ) <_ ( normop ` T ) ) -> 0 <_ ( normop ` T ) ) )
17 15 16 mp3an1 
 |-  ( ( ( normh ` ( T ` 0h ) ) e. RR* /\ ( normop ` T ) e. RR* ) -> ( ( 0 <_ ( normh ` ( T ` 0h ) ) /\ ( normh ` ( T ` 0h ) ) <_ ( normop ` T ) ) -> 0 <_ ( normop ` T ) ) )
18 13 14 17 syl2anc 
 |-  ( T : ~H --> ~H -> ( ( 0 <_ ( normh ` ( T ` 0h ) ) /\ ( normh ` ( T ` 0h ) ) <_ ( normop ` T ) ) -> 0 <_ ( normop ` T ) ) )
19 5 10 18 mp2and 
 |-  ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )