Definition df-md 25821

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

Assertion

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

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-md

Step	Hyp	Ref	Expression
1		cmd 24505	. 2 class MH
2		vx	. . . . . . 7 setvar x
3	2	cv 1369	. . . . . 6 class x
4		cch 24468	. . . . . 6 class CH
5	3, 4	wcel 1758	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 setvar y
7	6	cv 1369	. . . . . 6 class y
8	7, 4	wcel 1758	. . . . 5 wff y e. CH
9	5, 8	wa 369	. . . 4 wff ( x e. CH /\ y e. CH )
10		vz	. . . . . . . 8 setvar z
11	10	cv 1369	. . . . . . 7 class z
12	11, 7	wss 3428	. . . . . 6 wff z C_ y
13		chj 24472	. . . . . . . . 9 class vH
14	11, 3, 13	co 6192	. . . . . . . 8 class ( z vH x )
15	14, 7	cin 3427	. . . . . . 7 class ( ( z vH x ) i^i y )
16	3, 7	cin 3427	. . . . . . . 8 class ( x i^i y )
17	11, 16, 13	co 6192	. . . . . . 7 class ( z vH ( x i^i y ) )
18	15, 17	wceq 1370	. . . . . 6 wff ( ( z vH x ) i^i y ) = ( z vH ( x i^i y ) )
19	12, 18	wi 4	. . . . 5 wff ( z C_ y -> ( ( z vH x ) i^i y ) = ( z vH ( x i^i y ) ) )
20	19, 10, 4	wral 2795	. . . 4 wff A. z e. CH ( z C_ y -> ( ( z vH x ) i^i y ) = ( z vH ( x i^i y ) ) )
21	9, 20	wa 369	. . 3 wff ( ( 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	21, 2, 6	copab 4449	. 2 class { <. 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 ) ) ) ) }
23	1, 22	wceq 1370	1 wff 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 ) ) ) ) }

This definition is referenced by:  mdbr  25835