Theorem atnem0

Description: The meet of distinct atoms is zero. ( atnemeq0 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atnem0.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	atnem0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	atnem0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atnem0	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P\ne Q\leftrightarrow P\underset{\dot{}}{\wedge }Q=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		atnem0.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
2		atnem0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		atnem0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5	4 3	atncmp	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(\neg P{\le }_{K}Q\leftrightarrow P\ne Q\right)$$
6		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
7	6 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
8	6 4 1 2 3	atnle	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in {\mathrm{Base}}_K\right)\to \left(\neg P{\le }_{K}Q\leftrightarrow P\underset{\dot{}}{\wedge }Q=\underset{\dot{}}{0}\right)$$
9	7 8	syl3an3	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(\neg P{\le }_{K}Q\leftrightarrow P\underset{\dot{}}{\wedge }Q=\underset{\dot{}}{0}\right)$$
10	5 9	bitr3d	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P\ne Q\leftrightarrow P\underset{\dot{}}{\wedge }Q=\underset{\dot{}}{0}\right)$$