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 SCHStatesACnormSA1

Proof

Step Hyp Ref Expression
1 choccl ACAC
2 hstcl SCHStatesACSA
3 1 2 sylan2 SCHStatesACSA
4 normcl SAnormSA
5 3 4 syl SCHStatesACnormSA
6 5 sqge0d SCHStatesAC0normSA2
7 hstcl SCHStatesACSA
8 normcl SAnormSA
9 7 8 syl SCHStatesACnormSA
10 9 resqcld SCHStatesACnormSA2
11 5 resqcld SCHStatesACnormSA2
12 10 11 addge01d SCHStatesAC0normSA2normSA2normSA2+normSA2
13 6 12 mpbid SCHStatesACnormSA2normSA2+normSA2
14 hstnmoc SCHStatesACnormSA2+normSA2=1
15 sq1 12=1
16 14 15 eqtr4di SCHStatesACnormSA2+normSA2=12
17 13 16 breqtrd SCHStatesACnormSA212
18 normge0 SA0normSA
19 7 18 syl SCHStatesAC0normSA
20 1re 1
21 0le1 01
22 le2sq normSA0normSA101normSA1normSA212
23 20 21 22 mpanr12 normSA0normSAnormSA1normSA212
24 9 19 23 syl2anc SCHStatesACnormSA1normSA212
25 17 24 mpbird SCHStatesACnormSA1