Metamath Proof Explorer

Theorem latlem12

Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011)

		Ref	Expression
	Hypotheses	latmle.b	$⊢ B = {Base}_{K}$
		latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
	Assertion	latlem12	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land X \underset{˙}{\leq} Z) \leftrightarrow X \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		latpos	$⊢ K \in Lat \to K \in Poset$
5	4	adantr	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Poset$
6		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
7		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
8		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
9		eqid	$⊢ join (K) = join (K)$
10		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
11	1 9 3 10 6 7	latcl2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (⟨Y, Z⟩ \in dom join (K) \land ⟨Y, Z⟩ \in dom \underset{˙}{\land})$
12	11	simprd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ⟨Y, Z⟩ \in dom \underset{˙}{\land}$
13	1 2 3 5 6 7 8 12	meetle	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land X \underset{˙}{\leq} Z) \leftrightarrow X \underset{˙}{\leq} (Y \underset{˙}{\land} Z))$