chdmj3

Description: De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chdmj3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} ⊥ (B)) = ⊥ (A) \cap B$

Step	Hyp	Ref	Expression
1		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
2		chdmj1	$⊢ (A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} ⊥ (B)) = ⊥ (A) \cap ⊥ (⊥ (B))$
3	1 2	sylan2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} ⊥ (B)) = ⊥ (A) \cap ⊥ (⊥ (B))$
4		ococ	$⊢ B \in C_{ℋ} \to ⊥ (⊥ (B)) = B$
5	4	adantl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (B)) = B$
6	5	ineq2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A) \cap ⊥ (⊥ (B)) = ⊥ (A) \cap B$
7	3 6	eqtrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} ⊥ (B)) = ⊥ (A) \cap B$

Metamath Proof Explorer