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

Definition df-hst 22752
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.)
Assertion
Ref Expression
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 )
) ) ) ) }
Distinct variable group:    x, f, y

Detailed syntax breakdown of Definition df-hst
StepHypRef Expression
1 chst 21503 . 2  class  CHStates
2 chil 21459 . . . . . . 7  class  ~H
3 vf . . . . . . . 8  set  f
43cv 1618 . . . . . . 7  class  f
52, 4cfv 4673 . . . . . 6  class  ( f `
 ~H )
6 cno 21463 . . . . . 6  class  normh
75, 6cfv 4673 . . . . 5  class  ( normh `  ( f `  ~H ) )
8 c1 8706 . . . . 5  class  1
97, 8wceq 1619 . . . 4  wff  ( normh `  ( f `  ~H ) )  =  1
10 vx . . . . . . . . 9  set  x
1110cv 1618 . . . . . . . 8  class  x
12 vy . . . . . . . . . 10  set  y
1312cv 1618 . . . . . . . . 9  class  y
14 cort 21470 . . . . . . . . 9  class  _|_
1513, 14cfv 4673 . . . . . . . 8  class  ( _|_ `  y )
1611, 15wss 3127 . . . . . . 7  wff  x  C_  ( _|_ `  y )
1711, 4cfv 4673 . . . . . . . . . 10  class  ( f `
 x )
1813, 4cfv 4673 . . . . . . . . . 10  class  ( f `
 y )
19 csp 21462 . . . . . . . . . 10  class  .ih
2017, 18, 19co 5792 . . . . . . . . 9  class  ( ( f `  x ) 
.ih  ( f `  y ) )
21 cc0 8705 . . . . . . . . 9  class  0
2220, 21wceq 1619 . . . . . . . 8  wff  ( ( f `  x ) 
.ih  ( f `  y ) )  =  0
23 chj 21473 . . . . . . . . . . 11  class  vH
2411, 13, 23co 5792 . . . . . . . . . 10  class  ( x  vH  y )
2524, 4cfv 4673 . . . . . . . . 9  class  ( f `
 ( x  vH  y ) )
26 cva 21460 . . . . . . . . . 10  class  +h
2717, 18, 26co 5792 . . . . . . . . 9  class  ( ( f `  x )  +h  ( f `  y ) )
2825, 27wceq 1619 . . . . . . . 8  wff  ( f `
 ( x  vH  y ) )  =  ( ( f `  x )  +h  (
f `  y )
)
2922, 28wa 360 . . . . . . 7  wff  ( ( ( f `  x
)  .ih  ( f `  y ) )  =  0  /\  ( f `
 ( x  vH  y ) )  =  ( ( f `  x )  +h  (
f `  y )
) )
3016, 29wi 6 . . . . . 6  wff  ( x 
C_  ( _|_ `  y
)  ->  ( (
( f `  x
)  .ih  ( f `  y ) )  =  0  /\  ( f `
 ( x  vH  y ) )  =  ( ( f `  x )  +h  (
f `  y )
) ) )
31 cch 21469 . . . . . 6  class  CH
3230, 12, 31wral 2518 . . . . 5  wff  A. y  e.  CH  ( x  C_  ( _|_ `  y )  ->  ( ( ( f `  x ) 
.ih  ( f `  y ) )  =  0  /\  ( f `
 ( x  vH  y ) )  =  ( ( f `  x )  +h  (
f `  y )
) ) )
3332, 10, 31wral 2518 . . . 4  wff  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 )
) ) )
349, 33wa 360 . . 3  wff  ( (
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 ) ) ) ) )
35 cmap 6740 . . . 4  class  ^m
362, 31, 35co 5792 . . 3  class  ( ~H 
^m  CH )
3734, 3, 36crab 2522 . 2  class  { 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 ) ) ) ) ) }
381, 37wceq 1619 1  wff  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 )
) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  ishst  22754
  Copyright terms: Public domain W3C validator