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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | choccl | |
|
2 | hstcl | |
|
3 | 1 2 | sylan2 | |
4 | normcl | |
|
5 | 3 4 | syl | |
6 | 5 | sqge0d | |
7 | hstcl | |
|
8 | normcl | |
|
9 | 7 8 | syl | |
10 | 9 | resqcld | |
11 | 5 | resqcld | |
12 | 10 11 | addge01d | |
13 | 6 12 | mpbid | |
14 | hstnmoc | |
|
15 | sq1 | |
|
16 | 14 15 | eqtr4di | |
17 | 13 16 | breqtrd | |
18 | normge0 | |
|
19 | 7 18 | syl | |
20 | 1re | |
|
21 | 0le1 | |
|
22 | le2sq | |
|
23 | 20 21 22 | mpanr12 | |
24 | 9 19 23 | syl2anc | |
25 | 17 24 | mpbird | |