Definition df-dmd 10332

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 <x,y> is a dual modular pair." See dmdbrt 10350 for membership relation.

Assertion

Ref	Expression
df-dmd	|- MH* = {<.x, y>. | ((x e. CH /\ y e. CH) /\ A.z e. CH (y (_ z -> ((z i^i x) vH y) = (z i^i (x vH y))))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-dmd

Step	Hyp	Ref	Expression
1		cdmd 9016	. 2 class MH*
2		vx	. . . . . . 7 set x
3	2	cv 1098	. . . . . 6 class x
4		cch 8978	. . . . . 6 class CH
5	3, 4	wcel 1105	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 set y
7	6	cv 1098	. . . . . 6 class y
8	7, 4	wcel 1105	. . . . 5 wff y e. CH
9	5, 8	wa 223	. . . 4 wff (x e. CH /\ y e. CH)
10		vz	. . . . . . . 8 set z
11	10	cv 1098	. . . . . . 7 class z
12	7, 11	wss 2018	. . . . . 6 wff y (_ z
13	11, 3	cin 2017	. . . . . . . 8 class (z i^i x)
14		chj 8982	. . . . . . . 8 class vH
15	13, 7, 14	co 3902	. . . . . . 7 class ((z i^i x) vH y)
16	3, 7, 14	co 3902	. . . . . . . 8 class (x vH y)
17	11, 16	cin 2017	. . . . . . 7 class (z i^i (x vH y))
18	15, 17	wceq 1099	. . . . . 6 wff ((z i^i x) vH y) = (z i^i (x vH y))
19	12, 18	wi 3	. . . . 5 wff (y (_ z -> ((z i^i x) vH y) = (z i^i (x vH y)))
20	19, 10, 4	wral 1621	. . . 4 wff A.z e. CH (y (_ z -> ((z i^i x) vH y) = (z i^i (x vH y)))
21	9, 20	wa 223	. . 3 wff ((x e. CH /\ y e. CH) /\ A.z e. CH (y (_ z -> ((z i^i x) vH y) = (z i^i (x vH y))))
22	21, 2, 6	copab 2634	. 2 class {<.x, y>. | ((x e. CH /\ y e. CH) /\ A.z e. CH (y (_ z -> ((z i^i x) vH y) = (z i^i (x vH y))))}
23	1, 22	wceq 1099	1 wff MH* = {<.x, y>. | ((x e. CH /\ y e. CH) /\ A.z e. CH (y (_ z -> ((z i^i x) vH y) = (z i^i (x vH y))))}

This definition is referenced by:  dmdbrt 10350

Copyright terms: Public domain