Metamath Proof Explorer

Definition df-hst

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

Ref Expression
Assertion 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 ) ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 chst 
 |-  CHStates
1 vf 
 |-  f
2 chba 
 |-  ~H
3 cmap 
 |-  ^m
4 cch 
 |-  CH
5 2 4 3 co 
 |-  ( ~H ^m CH )
6 cno 
 |-  normh
7 1 cv 
 |-  f
8 2 7 cfv 
 |-  ( f ` ~H )
9 8 6 cfv 
 |-  ( normh ` ( f ` ~H ) )
10 c1 
 |-  1
11 9 10 wceq 
 |-  ( normh ` ( f ` ~H ) ) = 1
12 vx 
 |-  x
13 vy 
 |-  y
14 12 cv 
 |-  x
15 cort 
 |-  _|_
16 13 cv 
 |-  y
17 16 15 cfv 
 |-  ( _|_ ` y )
18 14 17 wss 
 |-  x C_ ( _|_ ` y )
19 14 7 cfv 
 |-  ( f ` x )
20 csp 
 |-  .ih
21 16 7 cfv 
 |-  ( f ` y )
22 19 21 20 co 
 |-  ( ( f ` x ) .ih ( f ` y ) )
23 cc0 
 |-  0
24 22 23 wceq 
 |-  ( ( f ` x ) .ih ( f ` y ) ) = 0
25 chj 
 |-  vH
26 14 16 25 co 
 |-  ( x vH y )
27 26 7 cfv 
 |-  ( f ` ( x vH y ) )
28 cva 
 |-  +h
29 19 21 28 co 
 |-  ( ( f ` x ) +h ( f ` y ) )
30 27 29 wceq 
 |-  ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) )
31 24 30 wa 
 |-  ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) )
32 18 31 wi 
 |-  ( x C_ ( _|_ ` y ) -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) )
33 32 13 4 wral 
 |-  A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( f ` x ) .ih ( f ` y ) ) = 0 /\ ( f ` ( x vH y ) ) = ( ( f ` x ) +h ( f ` y ) ) ) )
34 33 12 4 wral 
 |-  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 ) ) ) )
35 11 34 wa 
 |-  ( ( 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 ) ) ) ) )
36 35 1 5 crab 
 |-  { 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 ) ) ) ) ) }
37 0 36 wceq 
 |-  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 ) ) ) ) ) }