Definition df-cm 9802

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 cmbri 9809 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 9080	. 2 class C_H
2		vx	. . . . . . 7 set x
3	2	cv 991	. . . . . 6 class x
4		cch 9073	. . . . . 6 class CH
5	3, 4	wcel 994	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 set y
7	6	cv 991	. . . . . 6 class y
8	7, 4	wcel 994	. . . . 5 wff y e. CH
9	5, 8	wa 221	. . . 4 wff (x e. CH /\ y e. CH)
10	3, 7	cin 2098	. . . . . 6 class (x i^i y)
11		cort 9074	. . . . . . . 8 class _|_
12	7, 11	cfv 3263	. . . . . . 7 class (_|_` y)
13	3, 12	cin 2098	. . . . . 6 class (x i^i (_|_` y))
14		chj 9077	. . . . . 6 class vH
15	10, 13, 14	co 4021	. . . . 5 class ((x i^i y) vH (x i^i (_|_` y)))
16	3, 15	wceq 992	. . . 4 wff x = ((x i^i y) vH (x i^i (_|_` y)))
17	9, 16	wa 221	. . 3 wff ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))
18	17, 2, 6	copab 2740	. 2 class {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}
19	1, 18	wceq 992	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:  cmbr 9803

Copyright terms: Public domain