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

Definition df-cm 23038
Description: Define the commutes relation (on the Hilbert lattice). Definition of commutes in [Kalmbach] p. 20, who uses the notation xCy for "x commutes with y." See cmbri 23045 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
df-cm  |-  C_H  =  { <. x ,  y
>.  |  ( (
x  e.  CH  /\  y  e.  CH )  /\  x  =  (
( x  i^i  y
)  vH  ( x  i^i  ( _|_ `  y
) ) ) ) }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-cm
StepHypRef Expression
1 ccm 22392 . 2  class  C_H
2 vx . . . . . . 7  set  x
32cv 1648 . . . . . 6  class  x
4 cch 22385 . . . . . 6  class  CH
53, 4wcel 1721 . . . . 5  wff  x  e. 
CH
6 vy . . . . . . 7  set  y
76cv 1648 . . . . . 6  class  y
87, 4wcel 1721 . . . . 5  wff  y  e. 
CH
95, 8wa 359 . . . 4  wff  ( x  e.  CH  /\  y  e.  CH )
103, 7cin 3279 . . . . . 6  class  ( x  i^i  y )
11 cort 22386 . . . . . . . 8  class  _|_
127, 11cfv 5413 . . . . . . 7  class  ( _|_ `  y )
133, 12cin 3279 . . . . . 6  class  ( x  i^i  ( _|_ `  y
) )
14 chj 22389 . . . . . 6  class  vH
1510, 13, 14co 6040 . . . . 5  class  ( ( x  i^i  y )  vH  ( x  i^i  ( _|_ `  y
) ) )
163, 15wceq 1649 . . . 4  wff  x  =  ( ( x  i^i  y )  vH  (
x  i^i  ( _|_ `  y ) ) )
179, 16wa 359 . . 3  wff  ( ( x  e.  CH  /\  y  e.  CH )  /\  x  =  (
( x  i^i  y
)  vH  ( x  i^i  ( _|_ `  y
) ) ) )
1817, 2, 6copab 4225 . 2  class  { <. x ,  y >.  |  ( ( x  e.  CH  /\  y  e.  CH )  /\  x  =  (
( x  i^i  y
)  vH  ( x  i^i  ( _|_ `  y
) ) ) ) }
191, 18wceq 1649 1  wff  C_H  =  { <. x ,  y
>.  |  ( (
x  e.  CH  /\  y  e.  CH )  /\  x  =  (
( x  i^i  y
)  vH  ( x  i^i  ( _|_ `  y
) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  cmbr  23039
  Copyright terms: Public domain W3C validator