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