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

Definition df-md 22854
Description: Define the 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 modular pair." See mdbr 22868 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
df-md  |-  MH  =  { <. x ,  y
>.  |  ( (
x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( z  C_  y  ->  ( ( z  vH  x )  i^i  y
)  =  ( z  vH  ( x  i^i  y ) ) ) ) }
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-md
StepHypRef Expression
1 cmd 21540 . 2  class  MH
2 vx . . . . . . 7  set  x
32cv 1624 . . . . . 6  class  x
4 cch 21503 . . . . . 6  class  CH
53, 4wcel 1687 . . . . 5  wff  x  e. 
CH
6 vy . . . . . . 7  set  y
76cv 1624 . . . . . 6  class  y
87, 4wcel 1687 . . . . 5  wff  y  e. 
CH
95, 8wa 360 . . . 4  wff  ( x  e.  CH  /\  y  e.  CH )
10 vz . . . . . . . 8  set  z
1110cv 1624 . . . . . . 7  class  z
1211, 7wss 3155 . . . . . 6  wff  z  C_  y
13 chj 21507 . . . . . . . . 9  class  vH
1411, 3, 13co 5821 . . . . . . . 8  class  ( z  vH  x )
1514, 7cin 3154 . . . . . . 7  class  ( ( z  vH  x )  i^i  y )
163, 7cin 3154 . . . . . . . 8  class  ( x  i^i  y )
1711, 16, 13co 5821 . . . . . . 7  class  ( z  vH  ( x  i^i  y ) )
1815, 17wceq 1625 . . . . . 6  wff  ( ( z  vH  x )  i^i  y )  =  ( z  vH  (
x  i^i  y )
)
1912, 18wi 6 . . . . 5  wff  ( z 
C_  y  ->  (
( z  vH  x
)  i^i  y )  =  ( z  vH  ( x  i^i  y
) ) )
2019, 10, 4wral 2546 . . . 4  wff  A. z  e.  CH  ( z  C_  y  ->  ( ( z  vH  x )  i^i  y )  =  ( z  vH  ( x  i^i  y ) ) )
219, 20wa 360 . . 3  wff  ( ( x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( z  C_  y  ->  ( ( z  vH  x )  i^i  y
)  =  ( z  vH  ( x  i^i  y ) ) ) )
2221, 2, 6copab 4079 . 2  class  { <. x ,  y >.  |  ( ( x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( z  C_  y  ->  ( ( z  vH  x )  i^i  y
)  =  ( z  vH  ( x  i^i  y ) ) ) ) }
231, 22wceq 1625 1  wff  MH  =  { <. x ,  y
>.  |  ( (
x  e.  CH  /\  y  e.  CH )  /\  A. z  e.  CH  ( z  C_  y  ->  ( ( z  vH  x )  i^i  y
)  =  ( z  vH  ( x  i^i  y ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  mdbr  22868
  Copyright terms: Public domain W3C validator