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 ) ) ) ) }