oldmm1

Description: De Morgan's law for meet in an ortholattice. ( chdmm1 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	oldmm1	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} Y) = \underset{˙}{⊥} (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		eqid	$⊢ \leq_{K} = \leq_{K}$
6		ollat	$⊢ K \in OL \to K \in Lat$
7	6	3ad2ant1	$⊢ (K \in OL \land X \in B \land Y \in B) \to K \in Lat$
8		olop	$⊢ K \in OL \to K \in OP$
9	8	3ad2ant1	$⊢ (K \in OL \land X \in B \land Y \in B) \to K \in OP$
10	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
11	6 10	syl3an1	$⊢ (K \in OL \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
12	1 4	opoccl	$⊢ (K \in OP \land X \underset{˙}{\land} Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} Y) \in B$
13	9 11 12	syl2anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} Y) \in B$
14	1 4	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
15	8 14	sylan	$⊢ (K \in OL \land X \in B) \to \underset{˙}{⊥} (X) \in B$
16	15	3adant3	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
17	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
18	8 17	sylan	$⊢ (K \in OL \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
19	18	3adant2	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
20	1 2	latjcl	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B$
21	7 16 19 20	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B$
22	1 5 2	latlej1	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (X) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
23	7 16 19 22	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
24		simp2	$⊢ (K \in OL \land X \in B \land Y \in B) \to X \in B$
25	1 5 4	oplecon1b	$⊢ (K \in OP \land X \in B \land \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B) \to (\underset{˙}{⊥} (X) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} X)$
26	9 24 21 25	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} X)$
27	23 26	mpbid	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} X$
28	1 5 2	latlej2	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
29	7 16 19 28	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
30		simp3	$⊢ (K \in OL \land X \in B \land Y \in B) \to Y \in B$
31	1 5 4	oplecon1b	$⊢ (K \in OP \land Y \in B \land \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B) \to (\underset{˙}{⊥} (Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} Y)$
32	9 30 21 31	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} Y)$
33	29 32	mpbid	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} Y$
34	1 4	opoccl	$⊢ (K \in OP \land \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \in B$
35	9 21 34	syl2anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \in B$
36	1 5 3	latlem12	$⊢ (K \in Lat \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \in B \land X \in B \land Y \in B)) \to ((\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} X \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} Y) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} (X \underset{˙}{\land} Y))$
37	7 35 24 30 36	syl13anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to ((\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} X \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} Y) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} (X \underset{˙}{\land} Y))$
38	27 33 37	mpbi2and	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} (X \underset{˙}{\land} Y)$
39	1 5 4	oplecon1b	$⊢ (K \in OP \land \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B \land X \underset{˙}{\land} Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} (X \underset{˙}{\land} Y) \leftrightarrow \underset{˙}{⊥} (X \underset{˙}{\land} Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)))$
40	9 21 11 39	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} (X \underset{˙}{\land} Y) \leftrightarrow \underset{˙}{⊥} (X \underset{˙}{\land} Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)))$
41	38 40	mpbid	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} Y) \leq_{K} (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
42	1 5 3	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} X$
43	6 42	syl3an1	$⊢ (K \in OL \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} X$
44	1 5 4	oplecon3b	$⊢ (K \in OP \land X \underset{˙}{\land} Y \in B \land X \in B) \to ((X \underset{˙}{\land} Y) \leq_{K} X \leftrightarrow \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y))$
45	9 11 24 44	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) \leq_{K} X \leftrightarrow \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y))$
46	43 45	mpbid	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y)$
47	1 5 3	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
48	6 47	syl3an1	$⊢ (K \in OL \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
49	1 5 4	oplecon3b	$⊢ (K \in OP \land X \underset{˙}{\land} Y \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) \leq_{K} Y \leftrightarrow \underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y))$
50	9 11 30 49	syl3anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) \leq_{K} Y \leftrightarrow \underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y))$
51	48 50	mpbid	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y)$
52	1 5 2	latjle12	$⊢ (K \in Lat \land (\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (Y) \in B \land \underset{˙}{⊥} (X \underset{˙}{\land} Y) \in B)) \to ((\underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y) \land \underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y)) \leftrightarrow (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y))$
53	7 16 19 13 52	syl13anc	$⊢ (K \in OL \land X \in B \land Y \in B) \to ((\underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y) \land \underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y)) \leftrightarrow (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y))$
54	46 51 53	mpbi2and	$⊢ (K \in OL \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leq_{K} \underset{˙}{⊥} (X \underset{˙}{\land} Y)$
55	1 5 7 13 21 41 54	latasymd	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} Y) = \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (Y)$

Metamath Proof Explorer

Theorem oldmm1

Proof