Metamath Proof Explorer

Theorem hstle1

Description: The norm of the value of a Hilbert-space-valued state is less than or equal to one. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstle1 
|- ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` A ) ) <_ 1 )

Proof

Step Hyp Ref Expression
1 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
2 hstcl 
 |-  ( ( S e. CHStates /\ ( _|_ ` A ) e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
3 1 2 sylan2 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
4 normcl 
 |-  ( ( S ` ( _|_ ` A ) ) e. ~H -> ( normh ` ( S ` ( _|_ ` A ) ) ) e. RR )
5 3 4 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` ( _|_ ` A ) ) ) e. RR )
6 5 sqge0d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> 0 <_ ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) )
7 hstcl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
8 normcl 
 |-  ( ( S ` A ) e. ~H -> ( normh ` ( S ` A ) ) e. RR )
9 7 8 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` A ) ) e. RR )
10 9 resqcld 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) e. RR )
11 5 resqcld 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) e. RR )
12 10 11 addge01d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( 0 <_ ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) ) )
13 6 12 mpbid 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) )
14 hstnmoc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = 1 )
15 sq1 
 |-  ( 1 ^ 2 ) = 1
16 14 15 eqtr4di 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = ( 1 ^ 2 ) )
17 13 16 breqtrd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( 1 ^ 2 ) )
18 normge0 
 |-  ( ( S ` A ) e. ~H -> 0 <_ ( normh ` ( S ` A ) ) )
19 7 18 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> 0 <_ ( normh ` ( S ` A ) ) )
20 1re 
 |-  1 e. RR
21 0le1 
 |-  0 <_ 1
22 le2sq 
 |-  ( ( ( ( normh ` ( S ` A ) ) e. RR /\ 0 <_ ( normh ` ( S ` A ) ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( normh ` ( S ` A ) ) <_ 1 <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
23 20 21 22 mpanr12 
 |-  ( ( ( normh ` ( S ` A ) ) e. RR /\ 0 <_ ( normh ` ( S ` A ) ) ) -> ( ( normh ` ( S ` A ) ) <_ 1 <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
24 9 19 23 syl2anc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) <_ 1 <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
25 17 24 mpbird 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` A ) ) <_ 1 )