Description: The norm of a Hilbert-space-valued state equals one iff the state value equals the state value of the lattice unit. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hst1h | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hstcl | |
|
2 | ax-hvaddid | |
|
3 | 1 2 | syl | |
4 | 3 | adantr | |
5 | ax-1cn | |
|
6 | choccl | |
|
7 | hstcl | |
|
8 | 6 7 | sylan2 | |
9 | normcl | |
|
10 | 8 9 | syl | |
11 | 10 | resqcld | |
12 | 11 | recnd | |
13 | pncan2 | |
|
14 | 5 12 13 | sylancr | |
15 | 14 | adantr | |
16 | oveq1 | |
|
17 | sq1 | |
|
18 | 16 17 | eqtr2di | |
19 | 18 | oveq1d | |
20 | hstnmoc | |
|
21 | 19 20 | sylan9eqr | |
22 | 21 | oveq1d | |
23 | 15 22 | eqtr3d | |
24 | 1m1e0 | |
|
25 | 23 24 | eqtrdi | |
26 | 25 | ex | |
27 | 10 | recnd | |
28 | sqeq0 | |
|
29 | 27 28 | syl | |
30 | norm-i | |
|
31 | 8 30 | syl | |
32 | 29 31 | bitrd | |
33 | 26 32 | sylibd | |
34 | 33 | imp | |
35 | 34 | oveq2d | |
36 | hstoc | |
|
37 | 36 | adantr | |
38 | 35 37 | eqtr3d | |
39 | 4 38 | eqtr3d | |
40 | fveq2 | |
|
41 | hst1a | |
|
42 | 41 | adantr | |
43 | 40 42 | sylan9eqr | |
44 | 39 43 | impbida | |