chdmj1

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

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

Step	Hyp	Ref	Expression
1		chdmm4	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (A) \cap ⊥ (B)) = A \lor_{ℋ} B$
2	1	fveq2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (⊥ (A) \cap ⊥ (B))) = ⊥ (A \lor_{ℋ} B)$
3		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
4		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
5		chincl	$⊢ (⊥ (A) \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to ⊥ (A) \cap ⊥ (B) \in C_{ℋ}$
6	3 4 5	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A) \cap ⊥ (B) \in C_{ℋ}$
7		ococ	$⊢ ⊥ (A) \cap ⊥ (B) \in C_{ℋ} \to ⊥ (⊥ (⊥ (A) \cap ⊥ (B))) = ⊥ (A) \cap ⊥ (B)$
8	6 7	syl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (⊥ (A) \cap ⊥ (B))) = ⊥ (A) \cap ⊥ (B)$
9	2 8	eqtr3d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} B) = ⊥ (A) \cap ⊥ (B)$

Metamath Proof Explorer