latmlem1

Description: Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		latmle.b	$⊢ B = {Base}_{K}$
2		latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
4	1 2 3	latmle1	$⊢ (K \in Lat \land X \in B \land Z \in B) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} X$
5	4	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} X$
6		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
7	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Z \in B) \to X \underset{˙}{\land} Z \in B$
8	7	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Z \in B$
9		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
10		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
11	1 2	lattr	$⊢ (K \in Lat \land (X \underset{˙}{\land} Z \in B \land X \in B \land Y \in B)) \to (((X \underset{˙}{\land} Z) \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$
12	6 8 9 10 11	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\land} Z) \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$
13	5 12	mpand	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$
14	1 2 3	latmle2	$⊢ (K \in Lat \land X \in B \land Z \in B) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
15	14	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
16	13 15	jctird	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to ((X \underset{˙}{\land} Z) \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z))$
17		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
18	8 10 17	3jca	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Z \in B \land Y \in B \land Z \in B)$
19	1 2 3	latlem12	$⊢ (K \in Lat \land (X \underset{˙}{\land} Z \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\land} Z) \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z) \leftrightarrow (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z))$
20	18 19	syldan	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\land} Z) \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Z) \underset{˙}{\leq} Z) \leftrightarrow (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z))$
21	16 20	sylibd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z))$

Metamath Proof Explorer

Theorem latmlem1

Proof