HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem hstlet 10157
Description: Ordering property of a Hilbert-space-valued state.
Assertion
Ref Expression
hstlet |- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ B)) -> (normh` (S` A)) <_ (normh` (S` B)))
Proof of Theorem hstlet
StepHypRef Expression
1 hstnmoct 10150 . . . . . . . 8 |- ((S e. CHStates /\ B e. CH) -> (((normh` (S` B))^2) + ((normh` (S` (_|_` B)))^2)) = 1)
21adantlr 393 . . . . . . 7 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> (((normh` (S` B))^2) + ((normh` (S` (_|_` B)))^2)) = 1)
32opreq2d 3976 . . . . . 6 |- (((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 add12t 5336 . . . . . . 7 |- ((((normh` (S` A))^2) e. CC /\ ((normh` (S` B))^2) e. CC /\ ((normh` (S` (_|_` B)))^2) e. CC) -> (((normh` (S` A))^2) + (((normh` (S` B))^2) + ((normh` (S` (_|_` B)))^2))) = (((normh` (S` B))^2) + (((normh` (S` A))^2) + ((normh` (S` (_|_` B)))^2))))
5 hstclt 10144 . . . . . . . . . . 11 |- ((S e. CHStates /\ A e. CH) -> (S` A) e. H~)
6 normclt 8991 . . . . . . . . . . 11 |- ((S` A) e. H~ -> (normh` (S` A)) e. RR)
75, 6syl 10 . . . . . . . . . 10 |- ((S e. CHStates /\ A e. CH) -> (normh` (S` A)) e. RR)
8 resqclt 6621 . . . . . . . . . 10 |- ((normh` (S` A)) e. RR -> ((normh` (S` A))^2) e. RR)
97, 8syl 10 . . . . . . . . 9 |- ((S e. CHStates /\ A e. CH) -> ((normh` (S` A))^2) e. RR)
109adantr 389 . . . . . . . 8 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> ((normh` (S` A))^2) e. RR)
1110recnd 5315 . . . . . . 7 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> ((normh` (S` A))^2) e. CC)
12 hstclt 10144 . . . . . . . . . . 11 |- ((S e. CHStates /\ B e. CH) -> (S` B) e. H~)
13 normclt 8991 . . . . . . . . . . 11 |- ((S` B) e. H~ -> (normh` (S` B)) e. RR)
1412, 13syl 10 . . . . . . . . . 10 |- ((S e. CHStates /\ B e. CH) -> (normh` (S` B)) e. RR)
15 resqclt 6621 . . . . . . . . . 10 |- ((normh` (S` B)) e. RR -> ((normh` (S` B))^2) e. RR)
1614, 15syl 10 . . . . . . . . 9 |- ((S e. CHStates /\ B e. CH) -> ((normh` (S` B))^2) e. RR)
1716adantlr 393 . . . . . . . 8 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> ((normh` (S` B))^2) e. RR)
1817recnd 5315 . . . . . . 7 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> ((normh` (S` B))^2) e. CC)
19 hstclt 10144 . . . . . . . . . . . 12 |- ((S e. CHStates /\ (_|_` B) e. CH) -> (S` (_|_` B)) e. H~)
20 chocclt 9184 . . . . . . . . . . . 12 |- (B e. CH -> (_|_` B) e. CH)
2119, 20sylan2 451 . . . . . . . . . . 11 |- ((S e. CHStates /\ B e. CH) -> (S` (_|_` B)) e. H~)
22 normclt 8991 . . . . . . . . . . 11 |- ((S` (_|_` B)) e. H~ -> (normh` (S` (_|_` B))) e. RR)
2321, 22syl 10 . . . . . . . . . 10 |- ((S e. CHStates /\ B e. CH) -> (normh` (S` (_|_` B))) e. RR)
24 resqclt 6621 . . . . . . . . . 10 |- ((normh` (S` (_|_` B))) e. RR -> ((normh` (S` (_|_` B)))^2) e. RR)
2523, 24syl 10 . . . . . . . . 9 |- ((S e. CHStates /\ B e. CH) -> ((normh` (S` (_|_` B)))^2) e. RR)
2625adantlr 393 . . . . . . . 8 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> ((normh` (S` (_|_` B)))^2) e. RR)
2726recnd 5315 . . . . . . 7 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> ((normh` (S` (_|_` B)))^2) e. CC)
284, 11, 18, 27syl3anc 858 . . . . . 6 |- (((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))))
293, 28eqtr3d 1509 . . . . 5 |- (((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))))
3029adantrr 395 . . . 4 |- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ B)) -> (((normh` (S` A))^2) + 1) = (((normh` (S` B))^2) + (((normh` (S` A))^2) + ((normh` (S` (_|_` B)))^2))))
31 hstpytht 10156 . . . . . . 7 |- (((S e. CHStates /\ A e. CH) /\ ((_|_` B) e. CH /\ A (_ (_|_` (_|_` B)))) -> ((normh` (S` (A vH (_|_` B))))^2) = (((normh` (S` A))^2) + ((normh` (S` (_|_` B)))^2)))
3220adantr 389 . . . . . . . 8 |- ((B e. CH /\ A (_ B) -> (_|_` B) e. CH)
33 ococt 9248 . . . . . . . . . 10 |- (B e. CH -> (_|_` (_|_` B)) = B)
3433sseq2d 2089 . . . . . . . . 9 |- (B e. CH -> (A (_ (_|_` (_|_` B)) <-> A (_ B))
3534biimpar 417 . . . . . . . 8 |- ((B e. CH /\ A (_ B) -> A (_ (_|_` (_|_` B)))
3632, 35jca 288 . . . . . . 7 |- ((B e. CH /\ A (_ B) -> ((_|_` B) e. CH /\ A (_ (_|_` (_|_` B))))
3731, 36sylan2 451 . . . . . 6 |- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ B)) -> ((normh` (S` (A vH (_|_` B))))^2) = (((normh` (S` A))^2) + ((normh` (S` (_|_` B)))^2)))
38 1re 5435 . . . . . . . . . 10 |- 1 e. RR
39 le2sqit 6632 . . . . . . . . . 10 |- ((((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))
4038, 39mpanr1 709 . . . . . . . . 9 |- ((((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))
41 hstclt 10144 . . . . . . . . . . . . 13 |- ((S e. CHStates /\ (A vH (_|_` B)) e. CH) -> (S` (A vH (_|_` B))) e. H~)
42 chjclt 9329 . . . . . . . . . . . . . 14 |- ((A e. CH /\ (_|_` B) e. CH) -> (A vH (_|_` B)) e. CH)
4342, 20sylan2 451 . . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> (A vH (_|_` B)) e. CH)
4441, 43sylan2 451 . . . . . . . . . . . 12 |- ((S e. CHStates /\ (A e. CH /\ B e. CH)) -> (S` (A vH (_|_` B))) e. H~)
4544anassrs 441 . . . . . . . . . . 11 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> (S` (A vH (_|_` B))) e. H~)
46 normclt 8991 . . . . . . . . . . 11 |- ((S` (A vH (_|_` B))) e. H~ -> (normh` (S` (A vH (_|_` B)))) e. RR)
4745, 46syl 10 . . . . . . . . . 10 |- (((S e. CHStates /\ A e. CH) /\ B e. CH) -> (normh` (S` (A vH (_|_` B)))) e. RR)
48 normge0t 8992 . . . . . . . . . . 11 |- ((S` (A vH (_|_` B))) e. H~