This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-dmd

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 is a dual modular pair." See dmdbr for membership relation. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdmd 
 |-  MH*
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 cch 
 |-  CH
5 3 4 wcel 
 |-  x e. CH
6 2 cv 
 |-  y
7 6 4 wcel 
 |-  y e. CH
8 5 7 wa 
 |-  ( x e. CH /\ y e. CH )
9 vz 
 |-  z
10 9 cv 
 |-  z
11 6 10 wss 
 |-  y C_ z
12 10 3 cin 
 |-  ( z i^i x )
13 chj 
 |-  vH
14 12 6 13 co 
 |-  ( ( z i^i x ) vH y )
15 3 6 13 co 
 |-  ( x vH y )
16 10 15 cin 
 |-  ( z i^i ( x vH y ) )
17 14 16 wceq 
 |-  ( ( z i^i x ) vH y ) = ( z i^i ( x vH y ) )
18 11 17 wi 
 |-  ( y C_ z -> ( ( z i^i x ) vH y ) = ( z i^i ( x vH y ) ) )
19 18 9 4 wral 
 |-  A. z e. CH ( y C_ z -> ( ( z i^i x ) vH y ) = ( z i^i ( x vH y ) ) )
20 8 19 wa 
 |-  ( ( 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 ) ) ) )
21 20 1 2 copab 
 |-  { <. 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 ) ) ) ) }
22 0 21 wceq 
 |-  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 ) ) ) ) }