mod2ile

Description: The weak direction of the modular law (e.g., pmod2iN ) 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	mod2ile	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{\leq} X \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} Z) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} 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 Z \underset{˙}{\leq} X) \to K \in Lat$
6		simplr3	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to Z \in B$
7		simplr2	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to Y \in B$
8		simplr1	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to X \in B$
9	6 7 8	3jca	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to (Z \in B \land Y \in B \land X \in B)$
10	5 9	jca	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to (K \in Lat \land (Z \in B \land Y \in B \land X \in B))$
11		simpr	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to Z \underset{˙}{\leq} X$
12	1 2 3 4	mod1ile	$⊢ (K \in Lat \land (Z \in B \land Y \in B \land X \in B)) \to (Z \underset{˙}{\leq} X \to (Z \underset{˙}{\lor} (Y \underset{˙}{\land} X)) \underset{˙}{\leq} ((Z \underset{˙}{\lor} Y) \underset{˙}{\land} X))$
13	10 11 12	sylc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to (Z \underset{˙}{\lor} (Y \underset{˙}{\land} X)) \underset{˙}{\leq} ((Z \underset{˙}{\lor} Y) \underset{˙}{\land} X)$
14	1 4	latmcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
15	5 8 7 14	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
16	15	oveq1d	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} Z = (Y \underset{˙}{\land} X) \underset{˙}{\lor} Z$
17	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land X \in B) \to Y \underset{˙}{\land} X \in B$
18	5 7 8 17	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to Y \underset{˙}{\land} X \in B$
19	1 3	latjcom	$⊢ (K \in Lat \land Y \underset{˙}{\land} X \in B \land Z \in B) \to (Y \underset{˙}{\land} X) \underset{˙}{\lor} Z = Z \underset{˙}{\lor} (Y \underset{˙}{\land} X)$
20	5 18 6 19	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to (Y \underset{˙}{\land} X) \underset{˙}{\lor} Z = Z \underset{˙}{\lor} (Y \underset{˙}{\land} X)$
21	16 20	eqtrd	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} Z = Z \underset{˙}{\lor} (Y \underset{˙}{\land} X)$
22	1 3	latjcom	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z = Z \underset{˙}{\lor} Y$
23	5 7 6 22	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to Y \underset{˙}{\lor} Z = Z \underset{˙}{\lor} Y$
24	23	oveq2d	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) = X \underset{˙}{\land} (Z \underset{˙}{\lor} Y)$
25	1 3	latjcl	$⊢ (K \in Lat \land Z \in B \land Y \in B) \to Z \underset{˙}{\lor} Y \in B$
26	5 6 7 25	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to Z \underset{˙}{\lor} Y \in B$
27	1 4	latmcom	$⊢ (K \in Lat \land X \in B \land Z \underset{˙}{\lor} Y \in B) \to X \underset{˙}{\land} (Z \underset{˙}{\lor} Y) = (Z \underset{˙}{\lor} Y) \underset{˙}{\land} X$
28	5 8 26 27	syl3anc	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to X \underset{˙}{\land} (Z \underset{˙}{\lor} Y) = (Z \underset{˙}{\lor} Y) \underset{˙}{\land} X$
29	24 28	eqtrd	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Z) = (Z \underset{˙}{\lor} Y) \underset{˙}{\land} X$
30	13 21 29	3brtr4d	$⊢ ((K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \land Z \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} Z) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z))$
31	30	ex	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{\leq} X \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} Z) \underset{˙}{\leq} (X \underset{˙}{\land} (Y \underset{˙}{\lor} Z)))$

Metamath Proof Explorer

Theorem mod2ile

Proof