Metamath Proof Explorer

Theorem cmbr2i

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pjoml2.1	$⊢ A \in C_{ℋ}$
		pjoml2.2	$⊢ B \in C_{ℋ}$
	Assertion	cmbr2i	$⊢ A 𝐶_{ℋ} B \leftrightarrow A = (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B))$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1 2	cmcm4i	$⊢ A 𝐶_{ℋ} B \leftrightarrow ⊥ (A) 𝐶_{ℋ} ⊥ (B)$
4	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
5	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
6	4 5	cmbri	$⊢ ⊥ (A) 𝐶_{ℋ} ⊥ (B) \leftrightarrow ⊥ (A) = (⊥ (A) \cap ⊥ (B)) \lor_{ℋ} (⊥ (A) \cap ⊥ (⊥ (B)))$
7		eqcom	$⊢ A = (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B)) \leftrightarrow (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B)) = A$
8	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
9	1 5	chjcli	$⊢ A \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
10	8 9	chincli	$⊢ (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B)) \in C_{ℋ}$
11	10 1	chcon3i	$⊢ (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B)) = A \leftrightarrow ⊥ (A) = ⊥ ((A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B)))$
12	8 9	chdmm1i	$⊢ ⊥ ((A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B))) = ⊥ (A \lor_{ℋ} B) \lor_{ℋ} ⊥ (A \lor_{ℋ} ⊥ (B))$
13	1 2	chdmj1i	$⊢ ⊥ (A \lor_{ℋ} B) = ⊥ (A) \cap ⊥ (B)$
14	1 5	chdmj1i	$⊢ ⊥ (A \lor_{ℋ} ⊥ (B)) = ⊥ (A) \cap ⊥ (⊥ (B))$
15	13 14	oveq12i	$⊢ ⊥ (A \lor_{ℋ} B) \lor_{ℋ} ⊥ (A \lor_{ℋ} ⊥ (B)) = (⊥ (A) \cap ⊥ (B)) \lor_{ℋ} (⊥ (A) \cap ⊥ (⊥ (B)))$
16	12 15	eqtri	$⊢ ⊥ ((A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B))) = (⊥ (A) \cap ⊥ (B)) \lor_{ℋ} (⊥ (A) \cap ⊥ (⊥ (B)))$
17	16	eqeq2i	$⊢ ⊥ (A) = ⊥ ((A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B))) \leftrightarrow ⊥ (A) = (⊥ (A) \cap ⊥ (B)) \lor_{ℋ} (⊥ (A) \cap ⊥ (⊥ (B)))$
18	7 11 17	3bitrri	$⊢ ⊥ (A) = (⊥ (A) \cap ⊥ (B)) \lor_{ℋ} (⊥ (A) \cap ⊥ (⊥ (B))) \leftrightarrow A = (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B))$
19	3 6 18	3bitri	$⊢ A 𝐶_{ℋ} B \leftrightarrow A = (A \lor_{ℋ} B) \cap (A \lor_{ℋ} ⊥ (B))$