mod1ile

Description: The weak direction of the modular law (e.g., pmod1i , atmod1i1 ) that holds in any lattice. (Contributed by NM, 11-May-2012)

	Ref	Expression
Hypotheses	modle.b	$⊢ B = {Base}_{K}$
	modle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	modle.j	$⊢ \underset{˙}{\lor} = join (K)$
	modle.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	mod1ile	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Z \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$

Proof

Step	Hyp	Ref	Expression
1		modle.b	$⊢ B = {Base}_{K}$
2		modle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		modle.j	$⊢ \underset{˙}{\lor} = join (K)$
4		modle.m	$⊢ \underset{˙}{\land} = meet (K)$
5		simpll	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to K \in Lat$
6		simplr1	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to X \in B$
7		simplr2	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to Y \in B$
8	1 2 3	latlej1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
9	5 6 7 8	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
10		simpr	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} Z$
11	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
12	5 6 7 11	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to X \underset{˙}{\lor} Y \in B$
13		simplr3	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to Z \in B$
14	1 2 4	latlem12	$⊢ (K \in Lat \land (X \in B \land X \underset{˙}{\lor} Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land X \underset{˙}{\leq} Z) \leftrightarrow X \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
15	5 6 12 13 14	syl13anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land X \underset{˙}{\leq} Z) \leftrightarrow X \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
16	9 10 15	mpbi2and	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)$
17	1 2 3 4	latmlej12	$⊢ (K \in Lat \land (Y \in B \land Z \in B \land X \in B)) \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
18	5 7 13 6 17	syl13anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
19	1 2 4	latmle2	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
20	5 7 13 19	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
21	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z \in B$
22	5 7 13 21	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to Y \underset{˙}{\land} Z \in B$
23	1 2 4	latlem12	$⊢ (K \in Lat \land (Y \underset{˙}{\land} Z \in B \land X \underset{˙}{\lor} Y \in B \land Z \in B)) \to (((Y \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land (Y \underset{˙}{\land} Z) \underset{˙}{\leq} Z) \leftrightarrow (Y \underset{˙}{\land} Z) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
24	5 22 12 13 23	syl13anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to (((Y \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land (Y \underset{˙}{\land} Z) \underset{˙}{\leq} Z) \leftrightarrow (Y \underset{˙}{\land} Z) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
25	18 20 24	mpbi2and	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)$
26	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
27	5 12 13 26	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
28	1 2 3	latjle12	$⊢ (K \in Lat \land (X \in B \land Y \underset{˙}{\land} Z \in B \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B)) \to ((X \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \land (Y \underset{˙}{\land} Z) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)) \leftrightarrow (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
29	5 6 22 27 28	syl13anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to ((X \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \land (Y \underset{˙}{\land} Z) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)) \leftrightarrow (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
30	16 25 29	mpbi2and	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{\leq} Z) \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)$
31	30	ex	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Z \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$

Metamath Proof Explorer

Theorem mod1ile

Proof