Definition df-cm 5493

Description: Define the commutes relation (on the Hilbert lattice). Definition of commutes in [Kalmbach] p. 20, who uses the notation xCy for "x commutes with y." See cmbr 5499 for membership relation.

Assertion

Ref	Expression
df-cm	|- Com = {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-cm

Step	Hyp	Ref	Expression
1		ccm 4975	. 2 class Com
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cch 4968	. . . . . 6 class CH
5	3, 4	wcel 1092	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. CH
9	5, 8	wa 196	. . . 4 wff (x e. CH /\ y e. CH)
10	3, 7	cin 1486	. . . . . 6 class (x i^i y)
11		cort 4969	. . . . . . . 8 class _|_
12	7, 11	cfv 2422	. . . . . . 7 class (_|_` y)
13	3, 12	cin 1486	. . . . . 6 class (x i^i (_|_` y))
14		chj 4972	. . . . . 6 class vH
15	10, 13, 14	co 3001	. . . . 5 class ((x i^i y) vH (x i^i (_|_` y)))
16	3, 15	wceq 1091	. . . 4 wff x = ((x i^i y) vH (x i^i (_|_` y)))
17	9, 16	wa 196	. . 3 wff ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))
18	17, 2, 6	copab 2055	. 2 class {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}
19	1, 18	wceq 1091	1 wff Com = {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}

This definition is referenced by:  cmbrt 5494

metamath.org