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	$⊢ 𝐶_{ℋ} = \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccm	$class 𝐶_{ℋ}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cch	$class C_{ℋ}$
5	3 4	wcel	$wff x \in C_{ℋ}$
6	2	cv	$setvar y$
7	6 4	wcel	$wff y \in C_{ℋ}$
8	5 7	wa	$wff (x \in C_{ℋ} \land y \in C_{ℋ})$
9	3 6	cin	$class (x \cap y)$
10		chj	$class \lor_{ℋ}$
11		cort	$class ⊥$
12	6 11	cfv	$class ⊥ (y)$
13	3 12	cin	$class (x \cap ⊥ (y))$
14	9 13 10	co	$class ((x \cap y) \lor_{ℋ} (x \cap ⊥ (y)))$
15	3 14	wceq	$wff x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y))$
16	8 15	wa	$wff ((x \in C_{ℋ} \land y \in C_{ℋ}) \land x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)))$
17	16 1 2	copab	$class \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)))\}$
18	0 17	wceq	$wff 𝐶_{ℋ} = \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land x = (x \cap y) \lor_{ℋ} (x \cap ⊥ (y)))\}$

Metamath Proof Explorer

Definition df-cm

Detailed syntax breakdown