Metamath Proof Explorer

Theorem oldmm2

Description: De Morgan's law for meet in an ortholattice. ( chdmm2 analog.) (Contributed by NM, 6-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	oldmm2	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = X \underset{˙}{\lor} \underset{˙}{⊥} (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 X \in B) \to \underset{˙}{⊥} (X) \in B$
7	5 6	sylan	$⊢ (K \in OL \land X \in B) \to \underset{˙}{⊥} (X) \in B$
8	7	3adant3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
9	1 2 3 4	oldmm1	$⊢ (K \in OL \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \underset{˙}{\lor} \underset{˙}{⊥} (Y)$
10	8 9	syld3an2	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \underset{˙}{\lor} \underset{˙}{⊥} (Y)$
11	1 4	opococ	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
12	5 11	sylan	$⊢ (K \in OL \land X \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
13	12	3adant3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
14	13	oveq1d	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \underset{˙}{\lor} \underset{˙}{⊥} (Y) = X \underset{˙}{\lor} \underset{˙}{⊥} (Y)$
15	10 14	eqtrd	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) = X \underset{˙}{\lor} \underset{˙}{⊥} (Y)$