Metamath Proof Explorer


Theorem hst1h

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 SCHStatesACnormSA=1SA=S

Proof

Step Hyp Ref Expression
1 hstcl SCHStatesACSA
2 ax-hvaddid SASA+0=SA
3 1 2 syl SCHStatesACSA+0=SA
4 3 adantr SCHStatesACnormSA=1SA+0=SA
5 ax-1cn 1
6 choccl ACAC
7 hstcl SCHStatesACSA
8 6 7 sylan2 SCHStatesACSA
9 normcl SAnormSA
10 8 9 syl SCHStatesACnormSA
11 10 resqcld SCHStatesACnormSA2
12 11 recnd SCHStatesACnormSA2
13 pncan2 1normSA21+normSA2-1=normSA2
14 5 12 13 sylancr SCHStatesAC1+normSA2-1=normSA2
15 14 adantr SCHStatesACnormSA=11+normSA2-1=normSA2
16 oveq1 normSA=1normSA2=12
17 sq1 12=1
18 16 17 eqtr2di normSA=11=normSA2
19 18 oveq1d normSA=11+normSA2=normSA2+normSA2
20 hstnmoc SCHStatesACnormSA2+normSA2=1
21 19 20 sylan9eqr SCHStatesACnormSA=11+normSA2=1
22 21 oveq1d SCHStatesACnormSA=11+normSA2-1=11
23 15 22 eqtr3d SCHStatesACnormSA=1normSA2=11
24 1m1e0 11=0
25 23 24 eqtrdi SCHStatesACnormSA=1normSA2=0
26 25 ex SCHStatesACnormSA=1normSA2=0
27 10 recnd SCHStatesACnormSA
28 sqeq0 normSAnormSA2=0normSA=0
29 27 28 syl SCHStatesACnormSA2=0normSA=0
30 norm-i SAnormSA=0SA=0
31 8 30 syl SCHStatesACnormSA=0SA=0
32 29 31 bitrd SCHStatesACnormSA2=0SA=0
33 26 32 sylibd SCHStatesACnormSA=1SA=0
34 33 imp SCHStatesACnormSA=1SA=0
35 34 oveq2d SCHStatesACnormSA=1SA+SA=SA+0
36 hstoc SCHStatesACSA+SA=S
37 36 adantr SCHStatesACnormSA=1SA+SA=S
38 35 37 eqtr3d SCHStatesACnormSA=1SA+0=S
39 4 38 eqtr3d SCHStatesACnormSA=1SA=S
40 fveq2 SA=SnormSA=normS
41 hst1a SCHStatesnormS=1
42 41 adantr SCHStatesACnormS=1
43 40 42 sylan9eqr SCHStatesACSA=SnormSA=1
44 39 43 impbida SCHStatesACnormSA=1SA=S