olm01

Description: Meet with lattice zero is zero. ( chm0 analog.) (Contributed by NM, 8-Nov-2011)

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

Proof

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		eqid	$⊢ \leq_{K} = \leq_{K}$
5		ollat	$⊢ K \in OL \to K \in Lat$
6	5	adantr	$⊢ (K \in OL \land X \in B) \to K \in Lat$
7		simpr	$⊢ (K \in OL \land X \in B) \to X \in B$
8		olop	$⊢ K \in OL \to K \in OP$
9	8	adantr	$⊢ (K \in OL \land X \in B) \to K \in OP$
10	1 3	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in B$
11	9 10	syl	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \in B$
12	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\land} \underset{˙}{0} \in B$
13	6 7 11 12	syl3anc	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} \underset{˙}{0} \in B$
14	1 4 2	latmle2	$⊢ (K \in Lat \land X \in B \land \underset{˙}{0} \in B) \to (X \underset{˙}{\land} \underset{˙}{0}) \leq_{K} \underset{˙}{0}$
15	6 7 11 14	syl3anc	$⊢ (K \in OL \land X \in B) \to (X \underset{˙}{\land} \underset{˙}{0}) \leq_{K} \underset{˙}{0}$
16	1 4 3	op0le	$⊢ (K \in OP \land X \in B) \to \underset{˙}{0} \leq_{K} X$
17	8 16	sylan	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \leq_{K} X$
18	1 4	latref	$⊢ (K \in Lat \land \underset{˙}{0} \in B) \to \underset{˙}{0} \leq_{K} \underset{˙}{0}$
19	6 11 18	syl2anc	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \leq_{K} \underset{˙}{0}$
20	1 4 2	latlem12	$⊢ (K \in Lat \land (\underset{˙}{0} \in B \land X \in B \land \underset{˙}{0} \in B)) \to ((\underset{˙}{0} \leq_{K} X \land \underset{˙}{0} \leq_{K} \underset{˙}{0}) \leftrightarrow \underset{˙}{0} \leq_{K} (X \underset{˙}{\land} \underset{˙}{0}))$
21	6 11 7 11 20	syl13anc	$⊢ (K \in OL \land X \in B) \to ((\underset{˙}{0} \leq_{K} X \land \underset{˙}{0} \leq_{K} \underset{˙}{0}) \leftrightarrow \underset{˙}{0} \leq_{K} (X \underset{˙}{\land} \underset{˙}{0}))$
22	17 19 21	mpbi2and	$⊢ (K \in OL \land X \in B) \to \underset{˙}{0} \leq_{K} (X \underset{˙}{\land} \underset{˙}{0})$
23	1 4 6 13 11 15 22	latasymd	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem olm01

Proof