Metamath Proof Explorer

Theorem hstoh

Description: A Hilbert-space-valued state orthogonal to the state of the lattice unit is zero. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstoh 
|- ( ( S e. CHStates /\ A e. CH /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( S ` A ) = 0h )

Proof

Step Hyp Ref Expression
1 hstcl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
2 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
3 hstcl 
 |-  ( ( S e. CHStates /\ ( _|_ ` A ) e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
4 2 3 sylan2 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
5 his7 
 |-  ( ( ( S ` A ) e. ~H /\ ( S ` A ) e. ~H /\ ( S ` ( _|_ ` A ) ) e. ~H ) -> ( ( S ` A ) .ih ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) = ( ( ( S ` A ) .ih ( S ` A ) ) + ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) ) )
6 1 1 4 5 syl3anc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) .ih ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) = ( ( ( S ` A ) .ih ( S ` A ) ) + ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) ) )
7 normsq 
 |-  ( ( S ` A ) e. ~H -> ( ( normh ` ( S ` A ) ) ^ 2 ) = ( ( S ` A ) .ih ( S ` A ) ) )
8 1 7 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) = ( ( S ` A ) .ih ( S ` A ) ) )
9 8 eqcomd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) .ih ( S ` A ) ) = ( ( normh ` ( S ` A ) ) ^ 2 ) )
10 ococ 
 |-  ( A e. CH -> ( _|_ ` ( _|_ ` A ) ) = A )
11 eqimss2 
 |-  ( ( _|_ ` ( _|_ ` A ) ) = A -> A C_ ( _|_ ` ( _|_ ` A ) ) )
12 10 11 syl 
 |-  ( A e. CH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
13 2 12 jca 
 |-  ( A e. CH -> ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) )
14 13 adantl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) )
15 hstorth 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) = 0 )
16 14 15 mpdan 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) = 0 )
17 9 16 oveq12d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( S ` A ) .ih ( S ` A ) ) + ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 0 ) )
18 normcl 
 |-  ( ( S ` A ) e. ~H -> ( normh ` ( S ` A ) ) e. RR )
19 1 18 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` A ) ) e. RR )
20 19 resqcld 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) e. RR )
21 20 recnd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) e. CC )
22 21 addid1d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + 0 ) = ( ( normh ` ( S ` A ) ) ^ 2 ) )
23 6 17 22 3eqtrrd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) = ( ( S ` A ) .ih ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) )
24 hstoc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )
25 24 oveq2d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) .ih ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) = ( ( S ` A ) .ih ( S ` ~H ) ) )
26 23 25 eqtrd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) = ( ( S ` A ) .ih ( S ` ~H ) ) )
27 id 
 |-  ( ( ( S ` A ) .ih ( S ` ~H ) ) = 0 -> ( ( S ` A ) .ih ( S ` ~H ) ) = 0 )
28 26 27 sylan9eq 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) = 0 )
29 28 3impa 
 |-  ( ( S e. CHStates /\ A e. CH /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( ( normh ` ( S ` A ) ) ^ 2 ) = 0 )
30 19 recnd 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( S ` A ) ) e. CC )
31 sqeq0 
 |-  ( ( normh ` ( S ` A ) ) e. CC -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) = 0 <-> ( normh ` ( S ` A ) ) = 0 ) )
32 30 31 syl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) = 0 <-> ( normh ` ( S ` A ) ) = 0 ) )
33 32 3adant3 
 |-  ( ( S e. CHStates /\ A e. CH /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) = 0 <-> ( normh ` ( S ` A ) ) = 0 ) )
34 29 33 mpbid 
 |-  ( ( S e. CHStates /\ A e. CH /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( normh ` ( S ` A ) ) = 0 )
35 hst0h 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )
36 35 3adant3 
 |-  ( ( S e. CHStates /\ A e. CH /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )
37 34 36 mpbid 
 |-  ( ( S e. CHStates /\ A e. CH /\ ( ( S ` A ) .ih ( S ` ~H ) ) = 0 ) -> ( S ` A ) = 0h )