HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-st Unicode version

Definition df-st 22783
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
StepHypRef Expression
1 cst 21534 . 2  class  States
2 chil 21491 . . . . . 6  class  ~H
3 vf . . . . . . 7  set  f
43cv 1623 . . . . . 6  class  f
52, 4cfv 5221 . . . . 5  class  ( f `
 ~H )
6 c1 8733 . . . . 5  class  1
75, 6wceq 1624 . . . 4  wff  ( f `
 ~H )  =  1
8 vx . . . . . . . . 9  set  x
98cv 1623 . . . . . . . 8  class  x
10 vy . . . . . . . . . 10  set  y
1110cv 1623 . . . . . . . . 9  class  y
12 cort 21502 . . . . . . . . 9  class  _|_
1311, 12cfv 5221 . . . . . . . 8  class  ( _|_ `  y )
149, 13wss 3153 . . . . . . 7  wff  x  C_  ( _|_ `  y )
15 chj 21505 . . . . . . . . . 10  class  vH
169, 11, 15co 5819 . . . . . . . . 9  class  ( x  vH  y )
1716, 4cfv 5221 . . . . . . . 8  class  ( f `
 ( x  vH  y ) )
189, 4cfv 5221 . . . . . . . . 9  class  ( f `
 x )
1911, 4cfv 5221 . . . . . . . . 9  class  ( f `
 y )
20 caddc 8735 . . . . . . . . 9  class  +
2118, 19, 20co 5819 . . . . . . . 8  class  ( ( f `  x )  +  ( f `  y ) )
2217, 21wceq 1624 . . . . . . 7  wff  ( f `
 ( x  vH  y ) )  =  ( ( f `  x )  +  ( f `  y ) )
2314, 22wi 6 . . . . . 6  wff  ( x 
C_  ( _|_ `  y
)  ->  ( f `  ( x  vH  y
) )  =  ( ( f `  x
)  +  ( f `
 y ) ) )
24 cch 21501 . . . . . 6  class  CH
2523, 10, 24wral 2544 . . . . 5  wff  A. y  e.  CH  ( x  C_  ( _|_ `  y )  ->  ( f `  ( x  vH  y
) )  =  ( ( f `  x
)  +  ( f `
 y ) ) )
2625, 8, 24wral 2544 . . . 4  wff  A. x  e.  CH  A. y  e. 
CH  ( x  C_  ( _|_ `  y )  ->  ( f `  ( x  vH  y
) )  =  ( ( f `  x
)  +  ( f `
 y ) ) )
277, 26wa 360 . . 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 8732 . . . . 5  class  0
29 cicc 10653 . . . . 5  class  [,]
3028, 6, 29co 5819 . . . 4  class  ( 0 [,] 1 )
31 cmap 6767 . . . 4  class  ^m
3230, 24, 31co 5819 . . 3  class  ( ( 0 [,] 1 )  ^m  CH )
3327, 3, 32crab 2548 . 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 ) ) ) ) }
341, 33wceq 1624 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 ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isst  22785
  Copyright terms: Public domain W3C validator