Metamath Proof Explorer

Theorem hstle

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

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

Proof

Step Hyp Ref Expression
1 hstnmoc 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) = 1 )
2 1 adantlr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) = 1 )
3 2 oveq2d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) )
4 hstcl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
5 normcl 
 |-  ( ( S ` A ) e. ~H -> ( normh ` ( S ` A ) ) e. RR )
6 4 5 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` A ) ) e. RR )
7 6 resqcld 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) e. RR )
8 7 adantr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) e. RR )
9 8 recnd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) e. CC )
10 hstcl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( S ` B ) e. ~H )
11 normcl 
 |-  ( ( S ` B ) e. ~H -> ( normh ` ( S ` B ) ) e. RR )
12 10 11 syl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( normh ` ( S ` B ) ) e. RR )
13 12 resqcld 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( ( normh ` ( S ` B ) ) ^ 2 ) e. RR )
14 13 adantlr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` B ) ) ^ 2 ) e. RR )
15 14 recnd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` B ) ) ^ 2 ) e. CC )
16 choccl 
 |-  ( B e. CH -> ( _|_ ` B ) e. CH )
17 hstcl 
 |-  ( ( S e. CHStates /\ ( _|_ ` B ) e. CH ) -> ( S ` ( _|_ ` B ) ) e. ~H )
18 16 17 sylan2 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( S ` ( _|_ ` B ) ) e. ~H )
19 normcl 
 |-  ( ( S ` ( _|_ ` B ) ) e. ~H -> ( normh ` ( S ` ( _|_ ` B ) ) ) e. RR )
20 18 19 syl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( normh ` ( S ` ( _|_ ` B ) ) ) e. RR )
21 20 resqcld 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) e. RR )
22 21 adantlr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) e. RR )
23 22 recnd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) e. CC )
24 9 15 23 add12d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) = ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) )
25 3 24 eqtr3d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) = ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) )
26 25 adantrr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) = ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) )
27 16 adantr 
 |-  ( ( B e. CH /\ A C_ B ) -> ( _|_ ` B ) e. CH )
28 ococ 
 |-  ( B e. CH -> ( _|_ ` ( _|_ ` B ) ) = B )
29 28 sseq2d 
 |-  ( B e. CH -> ( A C_ ( _|_ ` ( _|_ ` B ) ) <-> A C_ B ) )
30 29 biimpar 
 |-  ( ( B e. CH /\ A C_ B ) -> A C_ ( _|_ ` ( _|_ ` B ) ) )
31 27 30 jca 
 |-  ( ( B e. CH /\ A C_ B ) -> ( ( _|_ ` B ) e. CH /\ A C_ ( _|_ ` ( _|_ ` B ) ) ) )
32 hstpyth 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( ( _|_ ` B ) e. CH /\ A C_ ( _|_ ` ( _|_ ` B ) ) ) ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) )
33 31 32 sylan2 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) )
34 chjcl 
 |-  ( ( A e. CH /\ ( _|_ ` B ) e. CH ) -> ( A vH ( _|_ ` B ) ) e. CH )
35 16 34 sylan2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH ( _|_ ` B ) ) e. CH )
36 hstcl 
 |-  ( ( S e. CHStates /\ ( A vH ( _|_ ` B ) ) e. CH ) -> ( S ` ( A vH ( _|_ ` B ) ) ) e. ~H )
37 35 36 sylan2 
 |-  ( ( S e. CHStates /\ ( A e. CH /\ B e. CH ) ) -> ( S ` ( A vH ( _|_ ` B ) ) ) e. ~H )
38 37 anassrs 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( S ` ( A vH ( _|_ ` B ) ) ) e. ~H )
39 normcl 
 |-  ( ( S ` ( A vH ( _|_ ` B ) ) ) e. ~H -> ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) e. RR )
40 38 39 syl 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) e. RR )
41 normge0 
 |-  ( ( S ` ( A vH ( _|_ ` B ) ) ) e. ~H -> 0 <_ ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) )
42 38 41 syl 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> 0 <_ ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) )
43 hstle1 
 |-  ( ( S e. CHStates /\ ( A vH ( _|_ ` B ) ) e. CH ) -> ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) <_ 1 )
44 35 43 sylan2 
 |-  ( ( S e. CHStates /\ ( A e. CH /\ B e. CH ) ) -> ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) <_ 1 )
45 44 anassrs 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) <_ 1 )
46 1re 
 |-  1 e. RR
47 le2sq2 
 |-  ( ( ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) e. RR /\ 0 <_ ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ) /\ ( 1 e. RR /\ ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) <_ 1 ) ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) <_ ( 1 ^ 2 ) )
48 46 47 mpanr1 
 |-  ( ( ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) e. RR /\ 0 <_ ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ) /\ ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) <_ 1 ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) <_ ( 1 ^ 2 ) )
49 40 42 45 48 syl21anc 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) <_ ( 1 ^ 2 ) )
50 sq1 
 |-  ( 1 ^ 2 ) = 1
51 49 50 breqtrdi 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) <_ 1 )
52 51 adantrr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` ( A vH ( _|_ ` B ) ) ) ) ^ 2 ) <_ 1 )
53 33 52 eqbrtrrd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) <_ 1 )
54 8 22 readdcld 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) e. RR )
55 leadd2 
 |-  ( ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) e. RR /\ 1 e. RR /\ ( ( normh ` ( S ` B ) ) ^ 2 ) e. RR ) -> ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) <_ 1 <-> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
56 46 55 mp3an2 
 |-  ( ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) e. RR /\ ( ( normh ` ( S ` B ) ) ^ 2 ) e. RR ) -> ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) <_ 1 <-> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
57 54 14 56 syl2anc 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) <_ 1 <-> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
58 57 adantrr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) <_ 1 <-> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
59 53 58 mpbid 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( ( normh ` ( S ` B ) ) ^ 2 ) + ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` B ) ) ) ^ 2 ) ) ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) )
60 26 59 eqbrtrd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) )
61 leadd1 
 |-  ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) e. RR /\ ( ( normh ` ( S ` B ) ) ^ 2 ) e. RR /\ 1 e. RR ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) <-> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
62 46 61 mp3an3 
 |-  ( ( ( ( normh ` ( S ` A ) ) ^ 2 ) e. RR /\ ( ( normh ` ( S ` B ) ) ^ 2 ) e. RR ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) <-> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
63 8 14 62 syl2anc 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) <-> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
64 63 adantrr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) <-> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 1 ) <_ ( ( ( normh ` ( S ` B ) ) ^ 2 ) + 1 ) ) )
65 60 64 mpbird 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) )
66 normge0 
 |-  ( ( S ` A ) e. ~H -> 0 <_ ( normh ` ( S ` A ) ) )
67 4 66 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> 0 <_ ( normh ` ( S ` A ) ) )
68 6 67 jca 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) e. RR /\ 0 <_ ( normh ` ( S ` A ) ) ) )
69 68 adantr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` A ) ) e. RR /\ 0 <_ ( normh ` ( S ` A ) ) ) )
70 normge0 
 |-  ( ( S ` B ) e. ~H -> 0 <_ ( normh ` ( S ` B ) ) )
71 10 70 syl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> 0 <_ ( normh ` ( S ` B ) ) )
72 12 71 jca 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( ( normh ` ( S ` B ) ) e. RR /\ 0 <_ ( normh ` ( S ` B ) ) ) )
73 72 adantlr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` B ) ) e. RR /\ 0 <_ ( normh ` ( S ` B ) ) ) )
74 le2sq 
 |-  ( ( ( ( normh ` ( S ` A ) ) e. RR /\ 0 <_ ( normh ` ( S ` A ) ) ) /\ ( ( normh ` ( S ` B ) ) e. RR /\ 0 <_ ( normh ` ( S ` B ) ) ) ) -> ( ( normh ` ( S ` A ) ) <_ ( normh ` ( S ` B ) ) <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) ) )
75 69 73 74 syl2anc 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ B e. CH ) -> ( ( normh ` ( S ` A ) ) <_ ( normh ` ( S ` B ) ) <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) ) )
76 75 adantrr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( S ` A ) ) <_ ( normh ` ( S ` B ) ) <-> ( ( normh ` ( S ` A ) ) ^ 2 ) <_ ( ( normh ` ( S ` B ) ) ^ 2 ) ) )
77 65 76 mpbird 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( normh ` ( S ` A ) ) <_ ( normh ` ( S ` B ) ) )