atnem0

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

	Ref	Expression
Hypotheses	atnem0.m	$⊢ \underset{˙}{\land} = meet (K)$
	atnem0.z	$⊢ \underset{˙}{0} = 0. (K)$
	atnem0.a	$⊢ A = Atoms (K)$
Assertion	atnem0	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P \underset{˙}{\land} Q = \underset{˙}{0})$

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

Metamath Proof Explorer