Definition df-cm 9466

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

Assertion

Ref	Expression
df-cm	⊢ Cℋ = {⟨x, y⟩∣((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ x = ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y))))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-cm

Step	Hyp	Ref	Expression
1		ccm 8744	. 2 class Cℋ
2		vx	. . . . . . 7 set x
3	2	cv 953	. . . . . 6 class x
4		cch 8737	. . . . . 6 class Cℋ
5	3, 4	wcel 956	. . . . 5 wff x ∈ Cℋ
6		vy	. . . . . . 7 set y
7	6	cv 953	. . . . . 6 class y
8	7, 4	wcel 956	. . . . 5 wff y ∈ Cℋ
9	5, 8	wa 223	. . . 4 wff (x ∈ Cℋ ⋀ y ∈ Cℋ )
10	3, 7	cin 2042	. . . . . 6 class (x ∩ y)
11		cort 8738	. . . . . . . 8 class ⊥
12	7, 11	cfv 3177	. . . . . . 7 class (⊥ ‘y)
13	3, 12	cin 2042	. . . . . 6 class (x ∩ (⊥ ‘y))
14		chj 8741	. . . . . 6 class ∨ℋ
15	10, 13, 14	co 3954	. . . . 5 class ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y)))
16	3, 15	wceq 954	. . . 4 wff x = ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y)))
17	9, 16	wa 223	. . 3 wff ((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ x = ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y))))
18	17, 2, 6	copab 2661	. 2 class {⟨x, y⟩∣((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ x = ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y))))}
19	1, 18	wceq 954	1 wff Cℋ = {⟨x, y⟩∣((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ x = ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y))))}

This definition is referenced by:  cmbrt 9467

Copyright terms: Public domain