pjoml3i

Description: Variation of orthomodular law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
4	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
5	3 4	pjoml2i	$⊢ ⊥ (A) \subseteq ⊥ (B) \to ⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B)) = ⊥ (B)$
6	2 1	chsscon3i	$⊢ B \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (B)$
7		eqcom	$⊢ ⊥ (⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B))) = B \leftrightarrow B = ⊥ (⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B)))$
8	3	choccli	$⊢ ⊥ (⊥ (A)) \in C_{ℋ}$
9	8 4	chincli	$⊢ ⊥ (⊥ (A)) \cap ⊥ (B) \in C_{ℋ}$
10	1 9	chdmj2i	$⊢ ⊥ (⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B))) = A \cap ⊥ (⊥ (⊥ (A)) \cap ⊥ (B))$
11	3 2	chdmm4i	$⊢ ⊥ (⊥ (⊥ (A)) \cap ⊥ (B)) = ⊥ (A) \lor_{ℋ} B$
12	11	ineq2i	$⊢ A \cap ⊥ (⊥ (⊥ (A)) \cap ⊥ (B)) = A \cap (⊥ (A) \lor_{ℋ} B)$
13	10 12	eqtri	$⊢ ⊥ (⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B))) = A \cap (⊥ (A) \lor_{ℋ} B)$
14	13	eqeq1i	$⊢ ⊥ (⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B))) = B \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} B) = B$
15	3 9	chjcli	$⊢ ⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B)) \in C_{ℋ}$
16	2 15	chcon2i	$⊢ B = ⊥ (⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B))) \leftrightarrow ⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B)) = ⊥ (B)$
17	7 14 16	3bitr3i	$⊢ A \cap (⊥ (A) \lor_{ℋ} B) = B \leftrightarrow ⊥ (A) \lor_{ℋ} (⊥ (⊥ (A)) \cap ⊥ (B)) = ⊥ (B)$
18	5 6 17	3imtr4i	$⊢ B \subseteq A \to A \cap (⊥ (A) \lor_{ℋ} B) = B$

Metamath Proof Explorer