Metamath Proof Explorer

Theorem hstles

Description: Ordering property of a Hilbert-space-valued state. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstles 
|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` A ) ) = 1 -> ( normh ` ( S ` B ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( normh ` ( S ` A ) ) = 1 )
2 hstle 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( normh ` ( S ` A ) ) <_ ( normh ` ( S ` B ) ) )
3 2 adantr 
 |-  ( ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( normh ` ( S ` A ) ) <_ ( normh ` ( S ` B ) ) )
4 1 3 eqbrtrrd 
 |-  ( ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) /\ ( normh ` ( S ` A ) ) = 1 ) -> 1 <_ ( normh ` ( S ` B ) ) )
5 4 ex 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` A ) ) = 1 -> 1 <_ ( normh ` ( S ` B ) ) ) )
6 hstle1 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( normh ` ( S ` B ) ) <_ 1 )
7 6 ad2ant2r 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( normh ` ( S ` B ) ) <_ 1 )
8 5 7 jctild 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` A ) ) = 1 -> ( ( normh ` ( S ` B ) ) <_ 1 /\ 1 <_ ( normh ` ( S ` B ) ) ) ) )
9 hstcl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( S ` B ) e. ~H )
10 normcl 
 |-  ( ( S ` B ) e. ~H -> ( normh ` ( S ` B ) ) e. RR )
11 1re 
 |-  1 e. RR
12 letri3 
 |-  ( ( ( normh ` ( S ` B ) ) e. RR /\ 1 e. RR ) -> ( ( normh ` ( S ` B ) ) = 1 <-> ( ( normh ` ( S ` B ) ) <_ 1 /\ 1 <_ ( normh ` ( S ` B ) ) ) ) )
13 11 12 mpan2 
 |-  ( ( normh ` ( S ` B ) ) e. RR -> ( ( normh ` ( S ` B ) ) = 1 <-> ( ( normh ` ( S ` B ) ) <_ 1 /\ 1 <_ ( normh ` ( S ` B ) ) ) ) )
14 9 10 13 3syl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( ( normh ` ( S ` B ) ) = 1 <-> ( ( normh ` ( S ` B ) ) <_ 1 /\ 1 <_ ( normh ` ( S ` B ) ) ) ) )
15 14 ad2ant2r 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` B ) ) = 1 <-> ( ( normh ` ( S ` B ) ) <_ 1 /\ 1 <_ ( normh ` ( S ` B ) ) ) ) )
16 8 15 sylibrd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` A ) ) = 1 -> ( normh ` ( S ` B ) ) = 1 ) )