# 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 ) ) ) ) ) )`