Metamath Proof Explorer

Theorem oldmj3

Description: De Morgan's law for join in an ortholattice. ( chdmj3 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	oldmj3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (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	5	3ad2ant1	$⊢ (K \in OL \land X \in B \land Y \in B) \to K \in OP$
7		simp3	$⊢ (K \in OL \land X \in B \land Y \in B) \to Y \in B$
8	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
9	6 7 8	syl2anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
10	1 2 3 4	oldmj1	$⊢ (K \in OL \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
11	9 10	syld3an3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
12	1 4	opococ	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
13	6 7 12	syl2anc	$⊢ (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 \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} Y$
15	11 14	eqtrd	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} Y$