cmbr3i

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1 2	cmcmi	$⊢ A 𝐶_{ℋ} B \leftrightarrow B 𝐶_{ℋ} A$
4	2 1	cmbr2i	$⊢ B 𝐶_{ℋ} A \leftrightarrow B = (B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A))$
5	3 4	bitri	$⊢ A 𝐶_{ℋ} B \leftrightarrow B = (B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A))$
6		ineq2	$⊢ B = (B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A)) \to A \cap B = A \cap ((B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A)))$
7		inass	$⊢ (A \cap (B \lor_{ℋ} A)) \cap (B \lor_{ℋ} ⊥ (A)) = A \cap ((B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A)))$
8	2 1	chjcomi	$⊢ B \lor_{ℋ} A = A \lor_{ℋ} B$
9	8	ineq2i	$⊢ A \cap (B \lor_{ℋ} A) = A \cap (A \lor_{ℋ} B)$
10	1 2	chabs2i	$⊢ A \cap (A \lor_{ℋ} B) = A$
11	9 10	eqtri	$⊢ A \cap (B \lor_{ℋ} A) = A$
12	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
13	2 12	chjcomi	$⊢ B \lor_{ℋ} ⊥ (A) = ⊥ (A) \lor_{ℋ} B$
14	11 13	ineq12i	$⊢ (A \cap (B \lor_{ℋ} A)) \cap (B \lor_{ℋ} ⊥ (A)) = A \cap (⊥ (A) \lor_{ℋ} B)$
15	7 14	eqtr3i	$⊢ A \cap ((B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A))) = A \cap (⊥ (A) \lor_{ℋ} B)$
16	6 15	eqtr2di	$⊢ B = (B \lor_{ℋ} A) \cap (B \lor_{ℋ} ⊥ (A)) \to A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B$
17	5 16	sylbi	$⊢ A 𝐶_{ℋ} B \to A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B$
18		inss1	$⊢ A \cap ⊥ (B) \subseteq A$
19	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
20	1 19	chincli	$⊢ A \cap ⊥ (B) \in C_{ℋ}$
21	20 1	pjoml2i	$⊢ A \cap ⊥ (B) \subseteq A \to (A \cap ⊥ (B)) \lor_{ℋ} (⊥ (A \cap ⊥ (B)) \cap A) = A$
22	18 21	ax-mp	$⊢ (A \cap ⊥ (B)) \lor_{ℋ} (⊥ (A \cap ⊥ (B)) \cap A) = A$
23	20	choccli	$⊢ ⊥ (A \cap ⊥ (B)) \in C_{ℋ}$
24	23 1	chincli	$⊢ ⊥ (A \cap ⊥ (B)) \cap A \in C_{ℋ}$
25	20 24	chjcomi	$⊢ (A \cap ⊥ (B)) \lor_{ℋ} (⊥ (A \cap ⊥ (B)) \cap A) = (⊥ (A \cap ⊥ (B)) \cap A) \lor_{ℋ} (A \cap ⊥ (B))$
26	22 25	eqtr3i	$⊢ A = (⊥ (A \cap ⊥ (B)) \cap A) \lor_{ℋ} (A \cap ⊥ (B))$
27	1 2	chdmm3i	$⊢ ⊥ (A \cap ⊥ (B)) = ⊥ (A) \lor_{ℋ} B$
28	27	ineq2i	$⊢ A \cap ⊥ (A \cap ⊥ (B)) = A \cap (⊥ (A) \lor_{ℋ} B)$
29		incom	$⊢ A \cap ⊥ (A \cap ⊥ (B)) = ⊥ (A \cap ⊥ (B)) \cap A$
30	28 29	eqtr3i	$⊢ A \cap (⊥ (A) \lor_{ℋ} B) = ⊥ (A \cap ⊥ (B)) \cap A$
31	30	eqeq1i	$⊢ A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B \leftrightarrow ⊥ (A \cap ⊥ (B)) \cap A = A \cap B$
32		oveq1	$⊢ ⊥ (A \cap ⊥ (B)) \cap A = A \cap B \to (⊥ (A \cap ⊥ (B)) \cap A) \lor_{ℋ} (A \cap ⊥ (B)) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
33	31 32	sylbi	$⊢ A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B \to (⊥ (A \cap ⊥ (B)) \cap A) \lor_{ℋ} (A \cap ⊥ (B)) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
34	26 33	eqtrid	$⊢ A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B \to A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
35	1 2	cmbri	$⊢ A 𝐶_{ℋ} B \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
36	34 35	sylibr	$⊢ A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B \to A 𝐶_{ℋ} B$
37	17 36	impbii	$⊢ A 𝐶_{ℋ} B \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} B) = A \cap B$

Metamath Proof Explorer

Theorem cmbr3i

Proof