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

Metamath Proof Explorer

Definition df-md

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 is a modular pair." See mdbr for membership relation. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

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

Detailed syntax breakdown

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