cmcm2i

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. (Contributed by NM, 4-Nov-2000) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
4	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
5	1 4	chincli	$⊢ A \cap ⊥ (B) \in C_{ℋ}$
6	3 5	chjcomi	$⊢ (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) = (A \cap ⊥ (B)) \lor_{ℋ} (A \cap B)$
7	2	pjococi	$⊢ ⊥ (⊥ (B)) = B$
8	7	ineq2i	$⊢ A \cap ⊥ (⊥ (B)) = A \cap B$
9	8	oveq2i	$⊢ (A \cap ⊥ (B)) \lor_{ℋ} (A \cap ⊥ (⊥ (B))) = (A \cap ⊥ (B)) \lor_{ℋ} (A \cap B)$
10	6 9	eqtr4i	$⊢ (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) = (A \cap ⊥ (B)) \lor_{ℋ} (A \cap ⊥ (⊥ (B)))$
11	10	eqeq2i	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \leftrightarrow A = (A \cap ⊥ (B)) \lor_{ℋ} (A \cap ⊥ (⊥ (B)))$
12	1 2	cmbri	$⊢ A 𝐶_{ℋ} B \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
13	1 4	cmbri	$⊢ A 𝐶_{ℋ} ⊥ (B) \leftrightarrow A = (A \cap ⊥ (B)) \lor_{ℋ} (A \cap ⊥ (⊥ (B)))$
14	11 12 13	3bitr4i	$⊢ A 𝐶_{ℋ} B \leftrightarrow A 𝐶_{ℋ} ⊥ (B)$

Metamath Proof Explorer