omlfh1N

Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in Kalmbach p. 25. ( fh1 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omlfh1.b	$⊢ B = {Base}_{K}$
	omlfh1.j	$⊢ \underset{˙}{\lor} = join (K)$
	omlfh1.m	$⊢ \underset{˙}{\land} = meet (K)$
	omlfh1.c	$⊢ C = cm (K)$
Assertion	omlfh1N	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)$

Proof

Step	Hyp	Ref	Expression
1		omlfh1.b	$⊢ B = {Base}_{K}$
2		omlfh1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		omlfh1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		omlfh1.c	$⊢ C = cm (K)$
5		omllat	$⊢ K \in OML \to K \in Lat$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7	1 6 2 3	latledi	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \leq_{K} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
8	5 7	sylan	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \leq_{K} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
9	8	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \leq_{K} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
10	5	adantr	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
11		simpr1	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
12		simpr2	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
13		simpr3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
14	1 2	latjcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z \in B$
15	10 12 13 14	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\lor} Z \in B$
16	1 3	latmcom	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\lor} Z \in B) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} X$
17	10 11 15 16	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} X$
18		omlol	$⊢ K \in OML \to K \in OL$
19	18	adantr	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to K \in OL$
20	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
21	10 11 12 20	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Y \in B$
22	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Z \in B) \to X \underset{˙}{\land} Z \in B$
23	10 11 13 22	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Z \in B$
24		eqid	$⊢ oc (K) = oc (K)$
25	1 2 3 24	oldmj1	$⊢ (K \in OL \land X \underset{˙}{\land} Y \in B \land X \underset{˙}{\land} Z \in B) \to oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = oc (K) (X \underset{˙}{\land} Y) \underset{˙}{\land} oc (K) (X \underset{˙}{\land} Z)$
26	19 21 23 25	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = oc (K) (X \underset{˙}{\land} Y) \underset{˙}{\land} oc (K) (X \underset{˙}{\land} Z)$
27	1 2 3 24	oldmm1	$⊢ (K \in OL \land X \in B \land Y \in B) \to oc (K) (X \underset{˙}{\land} Y) = oc (K) (X) \underset{˙}{\lor} oc (K) (Y)$
28	19 11 12 27	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (X \underset{˙}{\land} Y) = oc (K) (X) \underset{˙}{\lor} oc (K) (Y)$
29	1 2 3 24	oldmm1	$⊢ (K \in OL \land X \in B \land Z \in B) \to oc (K) (X \underset{˙}{\land} Z) = oc (K) (X) \underset{˙}{\lor} oc (K) (Z)$
30	19 11 13 29	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (X \underset{˙}{\land} Z) = oc (K) (X) \underset{˙}{\lor} oc (K) (Z)$
31	28 30	oveq12d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (X \underset{˙}{\land} Y) \underset{˙}{\land} oc (K) (X \underset{˙}{\land} Z) = (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))$
32	26 31	eqtrd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))$
33	17 32	oveq12d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \underset{˙}{\land} oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} X) \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)))$
34	33	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \underset{˙}{\land} oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} X) \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)))$
35		omlop	$⊢ K \in OML \to K \in OP$
36	35	adantr	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to K \in OP$
37	1 24	opoccl	$⊢ (K \in OP \land X \in B) \to oc (K) (X) \in B$
38	36 11 37	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (X) \in B$
39	1 24	opoccl	$⊢ (K \in OP \land Y \in B) \to oc (K) (Y) \in B$
40	36 12 39	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (Y) \in B$
41	1 2	latjcl	$⊢ (K \in Lat \land oc (K) (X) \in B \land oc (K) (Y) \in B) \to oc (K) (X) \underset{˙}{\lor} oc (K) (Y) \in B$
42	10 38 40 41	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (X) \underset{˙}{\lor} oc (K) (Y) \in B$
43	1 24	opoccl	$⊢ (K \in OP \land Z \in B) \to oc (K) (Z) \in B$
44	36 13 43	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (Z) \in B$
45	1 2	latjcl	$⊢ (K \in Lat \land oc (K) (X) \in B \land oc (K) (Z) \in B) \to oc (K) (X) \underset{˙}{\lor} oc (K) (Z) \in B$
46	10 38 44 45	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (X) \underset{˙}{\lor} oc (K) (Z) \in B$
47	1 3	latmcl	$⊢ (K \in Lat \land oc (K) (X) \underset{˙}{\lor} oc (K) (Y) \in B \land oc (K) (X) \underset{˙}{\lor} oc (K) (Z) \in B) \to (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) \in B$
48	10 42 46 47	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) \in B$
49	1 3	latmassOLD	$⊢ (K \in OL \land (Y \underset{˙}{\lor} Z \in B \land X \in B \land (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) \in B)) \to ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} X) \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))))$
50	19 15 11 48 49	syl13anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} X) \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))))$
51	50	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} X) \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))))$
52	1 24 4	cmt2N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X C oc (K) (Y))$
53	52	3adant3r3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \leftrightarrow X C oc (K) (Y))$
54		simpl	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to K \in OML$
55	1 2 3 24 4	cmtbr3N	$⊢ (K \in OML \land X \in B \land oc (K) (Y) \in B) \to (X C oc (K) (Y) \leftrightarrow X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) = X \underset{˙}{\land} oc (K) (Y))$
56	54 11 40 55	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X C oc (K) (Y) \leftrightarrow X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) = X \underset{˙}{\land} oc (K) (Y))$
57	53 56	bitrd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \leftrightarrow X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) = X \underset{˙}{\land} oc (K) (Y))$
58	57	biimpa	$⊢ ((K \in OML \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) = X \underset{˙}{\land} oc (K) (Y)$
59	58	adantrr	$⊢ ((K \in OML \land (X \in B \land Y \in B \land Z \in B)) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) = X \underset{˙}{\land} oc (K) (Y)$
60	59	3impa	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) = X \underset{˙}{\land} oc (K) (Y)$
61	1 24 4	cmt2N	$⊢ (K \in OML \land X \in B \land Z \in B) \to (X C Z \leftrightarrow X C oc (K) (Z))$
62	61	3adant3r2	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X C Z \leftrightarrow X C oc (K) (Z))$
63	1 2 3 24 4	cmtbr3N	$⊢ (K \in OML \land X \in B \land oc (K) (Z) \in B) \to (X C oc (K) (Z) \leftrightarrow X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) = X \underset{˙}{\land} oc (K) (Z))$
64	54 11 44 63	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X C oc (K) (Z) \leftrightarrow X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) = X \underset{˙}{\land} oc (K) (Z))$
65	62 64	bitrd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X C Z \leftrightarrow X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) = X \underset{˙}{\land} oc (K) (Z))$
66	65	biimpa	$⊢ ((K \in OML \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) = X \underset{˙}{\land} oc (K) (Z)$
67	66	adantrl	$⊢ ((K \in OML \land (X \in B \land Y \in B \land Z \in B)) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) = X \underset{˙}{\land} oc (K) (Z)$
68	67	3impa	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)) = X \underset{˙}{\land} oc (K) (Z)$
69	60 68	oveq12d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y))) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (X \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\land} (X \underset{˙}{\land} oc (K) (Z))$
70	1 3	latmmdiN	$⊢ (K \in OL \land (X \in B \land oc (K) (X) \underset{˙}{\lor} oc (K) (Y) \in B \land oc (K) (X) \underset{˙}{\lor} oc (K) (Z) \in B)) \to X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y))) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)))$
71	19 11 42 46 70	syl13anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y))) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)))$
72	71	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Y))) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)))$
73	1 3	latmmdiN	$⊢ (K \in OL \land (X \in B \land oc (K) (Y) \in B \land oc (K) (Z) \in B)) \to X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)) = (X \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\land} (X \underset{˙}{\land} oc (K) (Z))$
74	19 11 40 44 73	syl13anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)) = (X \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\land} (X \underset{˙}{\land} oc (K) (Z))$
75	74	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)) = (X \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\land} (X \underset{˙}{\land} oc (K) (Z))$
76	69 72 75	3eqtr4d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))$
77	76	oveq2d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z)))) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)))$
78	1 3	latmcl	$⊢ (K \in Lat \land oc (K) (Y) \in B \land oc (K) (Z) \in B) \to oc (K) (Y) \underset{˙}{\land} oc (K) (Z) \in B$
79	10 40 44 78	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (Y) \underset{˙}{\land} oc (K) (Z) \in B$
80	1 3	latm12	$⊢ (K \in OL \land (Y \underset{˙}{\lor} Z \in B \land X \in B \land oc (K) (Y) \underset{˙}{\land} oc (K) (Z) \in B)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))) = X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)))$
81	19 15 11 79 80	syl13anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))) = X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)))$
82	81	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (X \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))) = X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)))$
83	51 77 82	3eqtrd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} X) \underset{˙}{\land} ((oc (K) (X) \underset{˙}{\lor} oc (K) (Y)) \underset{˙}{\land} (oc (K) (X) \underset{˙}{\lor} oc (K) (Z))) = X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)))$
84	1 2 3 24	oldmj1	$⊢ (K \in OL \land Y \in B \land Z \in B) \to oc (K) (Y \underset{˙}{\lor} Z) = oc (K) (Y) \underset{˙}{\land} oc (K) (Z)$
85	19 12 13 84	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to oc (K) (Y \underset{˙}{\lor} Z) = oc (K) (Y) \underset{˙}{\land} oc (K) (Z)$
86	85	oveq2d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} oc (K) (Y \underset{˙}{\lor} Z) = (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))$
87		eqid	$⊢ 0. (K) = 0. (K)$
88	1 24 3 87	opnoncon	$⊢ (K \in OP \land Y \underset{˙}{\lor} Z \in B) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} oc (K) (Y \underset{˙}{\lor} Z) = 0. (K)$
89	36 15 88	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} oc (K) (Y \underset{˙}{\lor} Z) = 0. (K)$
90	86 89	eqtr3d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z)) = 0. (K)$
91	90	oveq2d	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))) = X \underset{˙}{\land} 0. (K)$
92	1 3 87	olm01	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} 0. (K) = 0. (K)$
93	19 11 92	syl2anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} 0. (K) = 0. (K)$
94	91 93	eqtrd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))) = 0. (K)$
95	94	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} ((Y \underset{˙}{\lor} Z) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\land} oc (K) (Z))) = 0. (K)$
96	34 83 95	3eqtrd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \underset{˙}{\land} oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = 0. (K)$
97	1 2	latjcl	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land X \underset{˙}{\land} Z \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) \in B$
98	10 21 23 97	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) \in B$
99	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\lor} Z \in B) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) \in B$
100	10 11 15 99	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) \in B$
101	1 6 3 24 87	omllaw3	$⊢ (K \in OML \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) \in B \land X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) \in B) \to ((((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \leq_{K} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \land (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \underset{˙}{\land} oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = 0. (K)) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) = X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
102	54 98 100 101	syl3anc	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B)) \to ((((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \leq_{K} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \land (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \underset{˙}{\land} oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = 0. (K)) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) = X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
103	102	3adant3	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to ((((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \leq_{K} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \land (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)) \underset{˙}{\land} oc (K) ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) = 0. (K)) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) = X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
104	9 96 103	mp2and	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) = X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)$
105	104	eqcomd	$⊢ (K \in OML \land (X \in B \land Y \in B \land Z \in B) \land (X C Y \land X C Z)) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)$

Metamath Proof Explorer

Theorem omlfh1N

Proof