omllaw4

Description: Orthomodular law equivalent. Remark in Holland95 p. 223. (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	omllaw4.b	$⊢ B = {Base}_{K}$
	omllaw4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	omllaw4.m	$⊢ \underset{˙}{\land} = meet (K)$
	omllaw4.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	omllaw4	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y = X)$

Proof

Step	Hyp	Ref	Expression
1		omllaw4.b	$⊢ B = {Base}_{K}$
2		omllaw4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		omllaw4.m	$⊢ \underset{˙}{\land} = meet (K)$
4		omllaw4.o	$⊢ \underset{˙}{⊥} = oc (K)$
5		simp1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OML$
6		omlop	$⊢ K \in OML \to K \in OP$
7	6	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OP$
8		simp3	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \in B$
9	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
10	7 8 9	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
11		simp2	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \in B$
12	1 4	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
13	7 11 12	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
14		eqid	$⊢ join (K) = join (K)$
15	1 2 14 3 4	omllaw	$⊢ (K \in OML \land \underset{˙}{⊥} (Y) \in B \land \underset{˙}{⊥} (X) \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X) \to \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
16	5 10 13 15	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X) \to \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
17	1 2 4	oplecon3b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))$
18	6 17	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))$
19		omllat	$⊢ K \in OML \to K \in Lat$
20	19	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in Lat$
21	1 3	latmcl	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} Y \in B$
22	20 13 8 21	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} Y \in B$
23	1 4	opoccl	$⊢ (K \in OP \land \underset{˙}{⊥} (X) \underset{˙}{\land} Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \in B$
24	7 22 23	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \in B$
25	1 3	latmcl	$⊢ (K \in Lat \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y \in B$
26	20 24 8 25	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y \in B$
27	1 4	opcon3b	$⊢ (K \in OP \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y \in B \land X \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y = X \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y))$
28	7 26 11 27	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y = X \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y))$
29	1 14	latjcom	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \underset{˙}{\land} Y \in B \land \underset{˙}{⊥} (Y) \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) join (K) \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} Y)$
30	20 22 10 29	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) join (K) \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} Y)$
31		omlol	$⊢ K \in OML \to K \in OL$
32	31	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OL$
33	1 14 3 4	oldmm2	$⊢ (K \in OL \land \underset{˙}{⊥} (X) \underset{˙}{\land} Y \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y) = (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) join (K) \underset{˙}{⊥} (Y)$
34	32 22 8 33	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y) = (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) join (K) \underset{˙}{⊥} (Y)$
35	1 4	opococ	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
36	7 8 35	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
37	36	oveq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} Y$
38	37	oveq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} Y)$
39	30 34 38	3eqtr4d	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)))$
40	39	eqeq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y) \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
41	28 40	bitrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y = X \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) join (K) (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
42	16 18 41	3imtr4d	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \underset{˙}{\land} Y) \underset{˙}{\land} Y = X)$

Metamath Proof Explorer

Theorem omllaw4

Proof