chdmj2

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

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

Step	Hyp	Ref	Expression
1		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
2		chdmj1	$⊢ (⊥ (A) \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (A) \lor_{ℋ} B) = ⊥ (⊥ (A)) \cap ⊥ (B)$
3	1 2	sylan	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (A) \lor_{ℋ} B) = ⊥ (⊥ (A)) \cap ⊥ (B)$
4		ococ	$⊢ A \in C_{ℋ} \to ⊥ (⊥ (A)) = A$
5	4	ineq1d	$⊢ A \in C_{ℋ} \to ⊥ (⊥ (A)) \cap ⊥ (B) = A \cap ⊥ (B)$
6	5	adantr	$⊢ (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