Definition df-st 29070

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.)

Assertion

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

Distinct variable group:   x, f, y

Detailed syntax breakdown of Definition df-st

Step	Hyp	Ref	Expression
1		cst 27819	. 2 class States
2		chil 27776	. . . . . 6 class ~H
3		vf	. . . . . . 7 setvar f
4	3	cv 1482	. . . . . 6 class f
5	2, 4	cfv 5888	. . . . 5 class ( f ` ~H )
6		c1 9937	. . . . 5 class 1
7	5, 6	wceq 1483	. . . 4 wff ( f ` ~H ) = 1
8		vx	. . . . . . . . 9 setvar x
9	8	cv 1482	. . . . . . . 8 class x
10		vy	. . . . . . . . . 10 setvar y
11	10	cv 1482	. . . . . . . . 9 class y
12		cort 27787	. . . . . . . . 9 class _|_
13	11, 12	cfv 5888	. . . . . . . 8 class ( _|_ ` y )
14	9, 13	wss 3574	. . . . . . 7 wff x C_ ( _|_ ` y )
15		chj 27790	. . . . . . . . . 10 class vH
16	9, 11, 15	co 6650	. . . . . . . . 9 class ( x vH y )
17	16, 4	cfv 5888	. . . . . . . 8 class ( f ` ( x vH y ) )
18	9, 4	cfv 5888	. . . . . . . . 9 class ( f ` x )
19	11, 4	cfv 5888	. . . . . . . . 9 class ( f ` y )
20		caddc 9939	. . . . . . . . 9 class +
21	18, 19, 20	co 6650	. . . . . . . 8 class ( ( f ` x ) + ( f ` y ) )
22	17, 21	wceq 1483	. . . . . . 7 wff ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) )
23	14, 22	wi 4	. . . . . 6 wff ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) )
24		cch 27786	. . . . . 6 class CH
25	23, 10, 24	wral 2912	. . . . 5 wff A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) )
26	25, 8, 24	wral 2912	. . . 4 wff A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) )
27	7, 26	wa 384	. . 3 wff ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) )
28		cc0 9936	. . . . 5 class 0
29		cicc 12178	. . . . 5 class [,]
30	28, 6, 29	co 6650	. . . 4 class ( 0 [,] 1 )
31		cmap 7857	. . . 4 class ^m
32	30, 24, 31	co 6650	. . 3 class ( ( 0 [,] 1 ) ^m CH )
33	27, 3, 32	crab 2916	. 2 class { 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 ) ) ) ) }
34	1, 33	wceq 1483	1 wff 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 ) ) ) ) }

This definition is referenced by:  isst  29072