Metamath Proof Explorer

Theorem ishst

Description: Property of a complex Hilbert-space-valued state. Definition of CH-states in Mayet3 p. 9. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion ishst 
|- ( S e. CHStates <-> ( S : CH --> ~H /\ ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 chex 
 |-  CH e. _V
3 1 2 elmap 
 |-  ( S e. ( ~H ^m CH ) <-> S : CH --> ~H )
4 3 anbi1i 
 |-  ( ( S e. ( ~H ^m CH ) /\ ( ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) ) <-> ( S : CH --> ~H /\ ( ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) ) )
5 fveq1 
 |-  ( f = S -> ( f ` ~H ) = ( S ` ~H ) )
6 5 fveqeq2d 
 |-  ( f = S -> ( ( normh ` ( f ` ~H ) ) = 1 <-> ( normh ` ( S ` ~H ) ) = 1 ) )
7 fveq1 
 |-  ( f = S -> ( f ` x ) = ( S ` x ) )
8 fveq1 
 |-  ( f = S -> ( f ` y ) = ( S ` y ) )
9 7 8 oveq12d 
 |-  ( f = S -> ( ( f ` x ) .ih ( f ` y ) ) = ( ( S ` x ) .ih ( S ` y ) ) )
10 9 eqeq1d 
 |-  ( f = S -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 <-> ( ( S ` x ) .ih ( S ` y ) ) = 0 ) )
11 fveq1 
 |-  ( f = S -> ( f ` ( x vH y ) ) = ( S ` ( x vH y ) ) )
12 7 8 oveq12d 
 |-  ( f = S -> ( ( f ` x ) +h ( f ` y ) ) = ( ( S ` x ) +h ( S ` y ) ) )
13 11 12 eqeq12d 
 |-  ( f = S -> ( ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) <-> ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) )
14 10 13 anbi12d 
 |-  ( f = S -> ( ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) <-> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) )
15 14 imbi2d 
 |-  ( f = S -> ( ( x C_ ( _|_ ` y ) -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) ) <-> ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) )
16 15 2ralbidv 
 |-  ( f = S -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) ) <-> A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) )
17 6 16 anbi12d 
 |-  ( f = S -> ( ( ( normh ` ( f ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) ) ) <-> ( ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) ) )
18 df-hst 
 |-  CHStates = { f e. ( ~H ^m CH ) | ( ( normh ` ( f ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) ) ) }
19 17 18 elrab2 
 |-  ( S e. CHStates <-> ( S e. ( ~H ^m CH ) /\ ( ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) ) )
20 3anass 
 |-  ( ( S : CH --> ~H /\ ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) <-> ( S : CH --> ~H /\ ( ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) ) )
21 4 19 20 3bitr4i 
 |-  ( S e. CHStates <-> ( S : CH --> ~H /\ ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) )