Metamath Proof Explorer

Definition df-st

Description: Define the set of states on a Hilbert lattice. Definition of Kalmbach p. 266. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion df-st 
|- States = { f e. ( ( 0 [,] 1 ) ^m CH ) | ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cst 
 |-  States
1 vf 
 |-  f
2 cc0 
 |-  0
3 cicc 
 |-  [,]
4 c1 
 |-  1
5 2 4 3 co 
 |-  ( 0 [,] 1 )
6 cmap 
 |-  ^m
7 cch 
 |-  CH
8 5 7 6 co 
 |-  ( ( 0 [,] 1 ) ^m CH )
9 1 cv 
 |-  f
10 chba 
 |-  ~H
11 10 9 cfv 
 |-  ( f ` ~H )
12 11 4 wceq 
 |-  ( f ` ~H ) = 1
13 vx 
 |-  x
14 vy 
 |-  y
15 13 cv 
 |-  x
16 cort 
 |-  _|_
17 14 cv 
 |-  y
18 17 16 cfv 
 |-  ( _|_ ` y )
19 15 18 wss 
 |-  x C_ ( _|_ ` y )
20 chj 
 |-  vH
21 15 17 20 co 
 |-  ( x vH y )
22 21 9 cfv 
 |-  ( f ` ( x vH y ) )
23 15 9 cfv 
 |-  ( f ` x )
24 caddc 
 |-  +
25 17 9 cfv 
 |-  ( f ` y )
26 23 25 24 co 
 |-  ( ( f ` x ) + ( f ` y ) )
27 22 26 wceq 
 |-  ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) )
28 19 27 wi 
 |-  ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) )
29 28 14 7 wral 
 |-  A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) )
30 29 13 7 wral 
 |-  A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) )
31 12 30 wa 
 |-  ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) )
32 31 1 8 crab 
 |-  { f e. ( ( 0 [,] 1 ) ^m CH ) | ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) ) }
33 0 32 wceq 
 |-  States = { f e. ( ( 0 [,] 1 ) ^m CH ) | ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) ) }