oldmj1

Description: De Morgan's law for join in an ortholattice. ( chdmj1 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	oldmj1	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} Y) = \underset{˙}{⊥} (X) \underset{˙}{\land} \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	1 2 3 4	oldmm4	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) = X \underset{˙}{\lor} Y$
6	5	fveq2d	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X \underset{˙}{\lor} Y)$
7		olop	$⊢ K \in OL \to K \in OP$
8	7	3ad2ant1	$⊢ (K \in OL \land X \in B \land Y \in B) \to K \in OP$
9		ollat	$⊢ K \in OL \to K \in Lat$
10	9	3ad2ant1	$⊢ (K \in OL \land X \in B \land Y \in B) \to K \in Lat$
11	1 4	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
12	7 11	sylan	$⊢ (K \in OL \land X \in B) \to \underset{˙}{⊥} (X) \in B$
13	12	3adant3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
14	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
15	7 14	sylan	$⊢ (K \in OL \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
16	15	3adant2	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
17	1 3	latmcl	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B$
18	10 13 16 17	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B$
19	1 4	opococ	$⊢ (K \in OP \land \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)$
20	8 18 19	syl2anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)$
21	6 20	eqtr3d	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} Y) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)$

Metamath Proof Explorer

Theorem oldmj1

Proof