latledi

Description: An ortholattice is distributive in one ordering direction. ( ledi analog.) (Contributed by NM, 7-Nov-2011)

	Ref	Expression
Hypotheses	latledi.b	$⊢ B = {Base}_{K}$
	latledi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	latledi.j	$⊢ \underset{˙}{\lor} = join (K)$
	latledi.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	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)) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$

Proof

Step	Hyp	Ref	Expression
1		latledi.b	$⊢ B = {Base}_{K}$
2		latledi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latledi.j	$⊢ \underset{˙}{\lor} = join (K)$
4		latledi.m	$⊢ \underset{˙}{\land} = meet (K)$
5	1 2 4	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
6	5	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
7	1 2 4	latmle1	$⊢ (K \in Lat \land X \in B \land Z \in B) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} X$
8	7	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} X$
9	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
10	9	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Y \in B$
11	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Z \in B) \to X \underset{˙}{\land} Z \in B$
12	11	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Z \in B$
13		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
14	10 12 13	3jca	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y \in B \land X \underset{˙}{\land} Z \in B \land X \in B)$
15	1 2 3	latjle12	$⊢ (K \in Lat \land (X \underset{˙}{\land} Y \in B \land X \underset{˙}{\land} Z \in B \land X \in B)) \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} X) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} X)$
16	14 15	syldan	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} X) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} X)$
17	6 8 16	mpbi2and	$⊢ (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)) \underset{˙}{\leq} X$
18	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
19	18	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
20	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land Z \in B) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
21	20	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
22		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
23		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
24		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
25	1 2 3	latjlej12	$⊢ (K \in Lat \land (X \underset{˙}{\land} Y \in B \land Y \in B) \land (X \underset{˙}{\land} Z \in B \land Z \in B)) \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
26	22 10 23 12 24 25	syl122anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
27	19 21 26	mp2and	$⊢ (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)) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)$
28	1 3	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$
29	22 10 12 28	syl3anc	$⊢ (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) \in B$
30	1 3	latjcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z \in B$
31	30	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\lor} Z \in B$
32	1 2 4	latlem12	$⊢ (K \in Lat \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z) \in B \land X \in B \land Y \underset{˙}{\lor} Z \in B)) \to ((((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} X \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)))$
33	22 29 13 31 32	syl13anc	$⊢ (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)) \underset{˙}{\leq} X \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} Z)) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)))$
34	17 27 33	mpbi2and	$⊢ (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)) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$

Metamath Proof Explorer

Theorem latledi

Proof