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 one. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hst1h 
|- ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 1 <-> ( S ` A ) = ( S ` ~H ) ) )

Proof

Step Hyp Ref Expression
1 hstcl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
2 ax-hvaddid 
 |-  ( ( S ` A ) e. ~H -> ( ( S ` A ) +h 0h ) = ( S ` A ) )
3 1 2 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h 0h ) = ( S ` A ) )
4 3 adantr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( S ` A ) +h 0h ) = ( S ` A ) )
5 ax-1cn 
 |-  1 e. CC
6 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
7 hstcl 
 |-  ( ( S e. CHStates /\ ( _|_ ` A ) e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
8 6 7 sylan2 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
9 normcl 
 |-  ( ( S ` ( _|_ ` A ) ) e. ~H -> ( normh ` ( S ` ( _|_ ` A ) ) ) e. RR )
10 8 9 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` ( _|_ ` A ) ) ) e. RR )
11 10 resqcld 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) e. RR )
12 11 recnd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) e. CC )
13 pncan2 
 |-  ( ( 1 e. CC /\ ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) e. CC ) -> ( ( 1 + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) - 1 ) = ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) )
14 5 12 13 sylancr 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( 1 + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) - 1 ) = ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) )
15 14 adantr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( 1 + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) - 1 ) = ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) )
16 oveq1 
 |-  ( ( normh ` ( S ` A ) ) = 1 -> ( ( normh ` ( S ` A ) ) ^ 2 ) = ( 1 ^ 2 ) )
17 sq1 
 |-  ( 1 ^ 2 ) = 1
18 16 17 eqtr2di 
 |-  ( ( normh ` ( S ` A ) ) = 1 -> 1 = ( ( normh ` ( S ` A ) ) ^ 2 ) )
19 18 oveq1d 
 |-  ( ( normh ` ( S ` A ) ) = 1 -> ( 1 + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) )
20 hstnmoc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = 1 )
21 19 20 sylan9eqr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( 1 + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = 1 )
22 21 oveq1d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( 1 + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) - 1 ) = ( 1 - 1 ) )
23 15 22 eqtr3d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) = ( 1 - 1 ) )
24 1m1e0 
 |-  ( 1 - 1 ) = 0
25 23 24 eqtrdi 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) = 0 )
26 25 ex 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 1 -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) = 0 ) )
27 10 recnd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` ( _|_ ` A ) ) ) e. CC )
28 sqeq0 
 |-  ( ( normh ` ( S ` ( _|_ ` A ) ) ) e. CC -> ( ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) = 0 <-> ( normh ` ( S ` ( _|_ ` A ) ) ) = 0 ) )
29 27 28 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) = 0 <-> ( normh ` ( S ` ( _|_ ` A ) ) ) = 0 ) )
30 norm-i 
 |-  ( ( S ` ( _|_ ` A ) ) e. ~H -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) = 0 <-> ( S ` ( _|_ ` A ) ) = 0h ) )
31 8 30 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` ( _|_ ` A ) ) ) = 0 <-> ( S ` ( _|_ ` A ) ) = 0h ) )
32 29 31 bitrd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) = 0 <-> ( S ` ( _|_ ` A ) ) = 0h ) )
33 26 32 sylibd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 1 -> ( S ` ( _|_ ` A ) ) = 0h ) )
34 33 imp 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( S ` ( _|_ ` A ) ) = 0h )
35 34 oveq2d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( ( S ` A ) +h 0h ) )
36 hstoc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )
37 36 adantr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )
38 35 37 eqtr3d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( ( S ` A ) +h 0h ) = ( S ` ~H ) )
39 4 38 eqtr3d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( normh ` ( S ` A ) ) = 1 ) -> ( S ` A ) = ( S ` ~H ) )
40 fveq2 
 |-  ( ( S ` A ) = ( S ` ~H ) -> ( normh ` ( S ` A ) ) = ( normh ` ( S ` ~H ) ) )
41 hst1a 
 |-  ( S e. CHStates -> ( normh ` ( S ` ~H ) ) = 1 )
42 41 adantr 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` ~H ) ) = 1 )
43 40 42 sylan9eqr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( S ` A ) = ( S ` ~H ) ) -> ( normh ` ( S ` A ) ) = 1 )
44 39 43 impbida 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 1 <-> ( S ` A ) = ( S ` ~H ) ) )