meetat

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012)

	Ref	Expression
Hypotheses	m.b	$⊢ B = {Base}_{K}$
	m.m	$⊢ \underset{˙}{\land} = meet (K)$
	m.z	$⊢ \underset{˙}{0} = 0. (K)$
	m.a	$⊢ A = Atoms (K)$
Assertion	meetat	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = P \lor X \underset{˙}{\land} P = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		m.b	$⊢ B = {Base}_{K}$
2		m.m	$⊢ \underset{˙}{\land} = meet (K)$
3		m.z	$⊢ \underset{˙}{0} = 0. (K)$
4		m.a	$⊢ A = Atoms (K)$
5		ollat	$⊢ K \in OL \to K \in Lat$
6	5	3ad2ant1	$⊢ (K \in OL \land X \in B \land P \in A) \to K \in Lat$
7		simp2	$⊢ (K \in OL \land X \in B \land P \in A) \to X \in B$
8		simp3	$⊢ (K \in OL \land X \in B \land P \in A) \to P \in A$
9	1 4	atbase	$⊢ P \in A \to P \in B$
10	8 9	syl	$⊢ (K \in OL \land X \in B \land P \in A) \to P \in B$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12	1 11 2	latmle2	$⊢ (K \in Lat \land X \in B \land P \in B) \to (X \underset{˙}{\land} P) \leq_{K} P$
13	6 7 10 12	syl3anc	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P) \leq_{K} P$
14		olop	$⊢ K \in OL \to K \in OP$
15	14	3ad2ant1	$⊢ (K \in OL \land X \in B \land P \in A) \to K \in OP$
16	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land P \in B) \to X \underset{˙}{\land} P \in B$
17	6 7 10 16	syl3anc	$⊢ (K \in OL \land X \in B \land P \in A) \to X \underset{˙}{\land} P \in B$
18	1 11 3 4	leatb	$⊢ (K \in OP \land X \underset{˙}{\land} P \in B \land P \in A) \to ((X \underset{˙}{\land} P) \leq_{K} P \leftrightarrow (X \underset{˙}{\land} P = P \lor X \underset{˙}{\land} P = \underset{˙}{0}))$
19	15 17 8 18	syl3anc	$⊢ (K \in OL \land X \in B \land P \in A) \to ((X \underset{˙}{\land} P) \leq_{K} P \leftrightarrow (X \underset{˙}{\land} P = P \lor X \underset{˙}{\land} P = \underset{˙}{0}))$
20	13 19	mpbid	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = P \lor X \underset{˙}{\land} P = \underset{˙}{0})$

Metamath Proof Explorer

Theorem meetat

Proof