latmlem2

Description: Add meet to both sides of a lattice ordering. ( sslin analog.) (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	latmlem2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (Z \underset{˙}{\land} X) \underset{˙}{\leq} (Z \underset{˙}{\land} Y))$

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	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))$
5	1 3	latmcom	$⊢ (K \in Lat \land X \in B \land Z \in B) \to X \underset{˙}{\land} Z = Z \underset{˙}{\land} X$
6	5	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Z = Z \underset{˙}{\land} X$
7	1 3	latmcom	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z = Z \underset{˙}{\land} Y$
8	7	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\land} Z = Z \underset{˙}{\land} Y$
9	6 8	breq12d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z) \leftrightarrow (Z \underset{˙}{\land} X) \underset{˙}{\leq} (Z \underset{˙}{\land} Y))$
10	4 9	sylibd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (Z \underset{˙}{\land} X) \underset{˙}{\leq} (Z \underset{˙}{\land} Y))$

Metamath Proof Explorer