Definition df-cm 9516

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 9523 for membership relation.

Assertion

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

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-cm

Step	Hyp	Ref	Expression
1		ccm 8789	. 2 class C_H
2		vx	. . . . . . 7 set x
3	2	cv 954	. . . . . 6 class x
4		cch 8782	. . . . . 6 class CH
5	3, 4	wcel 957	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 set y
7	6	cv 954	. . . . . 6 class y
8	7, 4	wcel 957	. . . . 5 wff y e. CH
9	5, 8	wa 223	. . . 4 wff (x e. CH /\ y e. CH)
10	3, 7	cin 2044	. . . . . 6 class (x i^i y)
11		cort 8783	. . . . . . . 8 class _|_
12	7, 11	cfv 3179	. . . . . . 7 class (_|_` y)
13	3, 12	cin 2044	. . . . . 6 class (x i^i (_|_` y))
14		chj 8786	. . . . . 6 class vH
15	10, 13, 14	co 3960	. . . . 5 class ((x i^i y) vH (x i^i (_|_` y)))
16	3, 15	wceq 955	. . . 4 wff x = ((x i^i y) vH (x i^i (_|_` y)))
17	9, 16	wa 223	. . 3 wff ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))
18	17, 2, 6	copab 2663	. 2 class {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}
19	1, 18	wceq 955	1 wff C_H = {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}

This definition is referenced by:  cmbrt 9517

Copyright terms: Public domain