olm02

Description: Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012)

	Ref	Expression
Hypotheses	olm0.b	$⊢ B = {Base}_{K}$
	olm0.m	$⊢ \underset{˙}{\land} = meet (K)$
	olm0.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	olm02	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \underset{˙}{\land} X = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		olm0.b	$⊢ B = {Base}_{K}$
2		olm0.m	$⊢ \underset{˙}{\land} = meet (K)$
3		olm0.z	$⊢ \underset{˙}{0} = 0. (K)$
4		ollat	$⊢ K \in OL \to K \in Lat$
5	4	adantr	$⊢ (K \in OL \land X \in B) \to K \in Lat$
6		simpr	$⊢ (K \in OL \land X \in B) \to X \in B$
7		olop	$⊢ K \in OL \to K \in OP$
8	7	adantr	$⊢ (K \in OL \land X \in B) \to K \in OP$
9	1 3	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in B$
10	8 9	syl	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \in B$
11	1 2	latmcom	$⊢ (K \in Lat \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\land} \underset{˙}{0} = \underset{˙}{0} \underset{˙}{\land} X$
12	5 6 10 11	syl3anc	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} \underset{˙}{0} = \underset{˙}{0} \underset{˙}{\land} X$
13	1 2 3	olm01	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} \underset{˙}{0} = \underset{˙}{0}$
14	12 13	eqtr3d	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \underset{˙}{\land} X = \underset{˙}{0}$

Metamath Proof Explorer