Metamath Proof Explorer

Theorem oldmj4

Description: De Morgan's law for join in an ortholattice. ( chdmj4 analog.) (Contributed by NM, 7-Nov-2011)

		Ref	Expression
	Hypotheses	oldmm1.b	$⊢ B = {Base}_{K}$
		oldmm1.j	$⊢ \underset{˙}{\lor} = join (K)$
		oldmm1.m	$⊢ \underset{˙}{\land} = meet (K)$
		oldmm1.o	$⊢ \underset{˙}{⊥} = oc (K)$
	Assertion	oldmj4	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X \underset{˙}{\land} Y$

Proof

Step	Hyp	Ref	Expression
1		oldmm1.b	$⊢ B = {Base}_{K}$
2		oldmm1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		oldmm1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		oldmm1.o	$⊢ \underset{˙}{⊥} = oc (K)$
5		olop	$⊢ K \in OL \to K \in OP$
6	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
7	5 6	sylan	$⊢ (K \in OL \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
8	7	3adant2	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
9	1 2 3 4	oldmj2	$⊢ (K \in OL \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
10	8 9	syld3an3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
11	1 4	opococ	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
12	5 11	sylan	$⊢ (K \in OL \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
13	12	3adant2	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
14	13	oveq2d	$⊢ (K \in OL \land X \in B \land Y \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = X \underset{˙}{\land} Y$
15	10 14	eqtrd	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X \underset{˙}{\land} Y$