Definition df-cm

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 for membership relation. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	df-cm	⊢ 𝐶ℋ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccm	⊢ 𝐶ℋ
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cch	⊢ Cℋ
5	3 4	wcel	⊢ 𝑥 ∈ Cℋ
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ Cℋ
8	5 7	wa	⊢ ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ )
9	3 6	cin	⊢ ( 𝑥 ∩ 𝑦 )
10		chj	⊢ ∨ℋ
11		cort	⊢ ⊥
12	6 11	cfv	⊢ ( ⊥ ‘ 𝑦 )
13	3 12	cin	⊢ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) )
14	9 13 10	co	⊢ ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) )
15	3 14	wceq	⊢ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) )
16	8 15	wa	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) )
17	16 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) }
18	0 17	wceq	⊢ 𝐶ℋ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) }