Theorem meetat2

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

	Ref	Expression
Hypotheses	m.b	$$⊢B={\mathrm{Base}}_K$$
	m.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	m.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	m.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	meetat2	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\wedge }P\in A\vee X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		m.b	$$⊢B={\mathrm{Base}}_K$$
2		m.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3		m.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		m.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5	1 2 3 4	meetat	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\wedge }P=P\vee X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\right)$$
6		eleq1a	$$⊢P\in A\to \left(X\underset{\dot{}}{\wedge }P=P\to X\underset{\dot{}}{\wedge }P\in A\right)$$
7	6	3ad2ant3	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\wedge }P=P\to X\underset{\dot{}}{\wedge }P\in A\right)$$
8	7	orim1d	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\wedge P\in A\right)\to \left(\left(X\underset{\dot{}}{\wedge }P=P\vee X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\right)\to \left(X\underset{\dot{}}{\wedge }P\in A\vee X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\right)\right)$$
9	5 8	mpd	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\wedge }P\in A\vee X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\right)$$