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

Definition df-dmd 22877
Description: Define the dual modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M* for "the ordered pair <x,y> is a dual modular pair." See dmdbr 22895 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-dmd  |-  MH*  =  { <. x ,  y
>.  |  ( (
x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( y  C_  z  ->  ( ( z  i^i  x )  vH  y
)  =  ( z  i^i  ( x  vH  y ) ) ) ) }
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-dmd
StepHypRef Expression
1 cdmd 21563 . 2  class  MH*
2 vx . . . . . . 7  set  x
32cv 1631 . . . . . 6  class  x
4 cch 21525 . . . . . 6  class  CH
53, 4wcel 1696 . . . . 5  wff  x  e. 
CH
6 vy . . . . . . 7  set  y
76cv 1631 . . . . . 6  class  y
87, 4wcel 1696 . . . . 5  wff  y  e. 
CH
95, 8wa 358 . . . 4  wff  ( x  e.  CH  /\  y  e.  CH )
10 vz . . . . . . . 8  set  z
1110cv 1631 . . . . . . 7  class  z
127, 11wss 3165 . . . . . 6  wff  y  C_  z
1311, 3cin 3164 . . . . . . . 8  class  ( z  i^i  x )
14 chj 21529 . . . . . . . 8  class  vH
1513, 7, 14co 5874 . . . . . . 7  class  ( ( z  i^i  x )  vH  y )
163, 7, 14co 5874 . . . . . . . 8  class  ( x  vH  y )
1711, 16cin 3164 . . . . . . 7  class  ( z  i^i  ( x  vH  y ) )
1815, 17wceq 1632 . . . . . 6  wff  ( ( z  i^i  x )  vH  y )  =  ( z  i^i  (
x  vH  y )
)
1912, 18wi 4 . . . . 5  wff  ( y 
C_  z  ->  (
( z  i^i  x
)  vH  y )  =  ( z  i^i  ( x  vH  y
) ) )
2019, 10, 4wral 2556 . . . 4  wff  A. z  e.  CH  ( y  C_  z  ->  ( ( z  i^i  x )  vH  y )  =  ( z  i^i  ( x  vH  y ) ) )
219, 20wa 358 . . 3  wff  ( ( x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( y  C_  z  ->  ( ( z  i^i  x )  vH  y
)  =  ( z  i^i  ( x  vH  y ) ) ) )
2221, 2, 6copab 4092 . 2  class  { <. x ,  y >.  |  ( ( x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( y  C_  z  ->  ( ( z  i^i  x )  vH  y
)  =  ( z  i^i  ( x  vH  y ) ) ) ) }
231, 22wceq 1632 1  wff  MH*  =  { <. x ,  y
>.  |  ( (
x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( y  C_  z  ->  ( ( z  i^i  x )  vH  y
)  =  ( z  i^i  ( x  vH  y ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  dmdbr  22895
  Copyright terms: Public domain W3C validator