atlltn0

Description: A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012)

	Ref	Expression
Hypotheses	atlltne0.b	$⊢ B = {Base}_{K}$
	atlltne0.s	$⊢ \underset{˙}{<} = <_{K}$
	atlltne0.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	atlltn0	$⊢ (K \in AtLat \land X \in B) \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow X \neq \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		atlltne0.b	$⊢ B = {Base}_{K}$
2		atlltne0.s	$⊢ \underset{˙}{<} = <_{K}$
3		atlltne0.z	$⊢ \underset{˙}{0} = 0. (K)$
4		simpl	$⊢ (K \in AtLat \land X \in B) \to K \in AtLat$
5	1 3	atl0cl	$⊢ K \in AtLat \to \underset{˙}{0} \in B$
6	5	adantr	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \in B$
7		simpr	$⊢ (K \in AtLat \land X \in B) \to X \in B$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	8 2	pltval	$⊢ (K \in AtLat \land \underset{˙}{0} \in B \land X \in B) \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow (\underset{˙}{0} \leq_{K} X \land \underset{˙}{0} \neq X))$
10	4 6 7 9	syl3anc	$⊢ (K \in AtLat \land X \in B) \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow (\underset{˙}{0} \leq_{K} X \land \underset{˙}{0} \neq X))$
11		necom	$⊢ X \neq \underset{˙}{0} \leftrightarrow \underset{˙}{0} \neq X$
12	1 8 3	atl0le	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \leq_{K} X$
13	12	biantrurd	$⊢ (K \in AtLat \land X \in B) \to (\underset{˙}{0} \neq X \leftrightarrow (\underset{˙}{0} \leq_{K} X \land \underset{˙}{0} \neq X))$
14	11 13	bitr2id	$⊢ (K \in AtLat \land X \in B) \to ((\underset{˙}{0} \leq_{K} X \land \underset{˙}{0} \neq X) \leftrightarrow X \neq \underset{˙}{0})$
15	10 14	bitrd	$⊢ (K \in AtLat \land X \in B) \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow X \neq \underset{˙}{0})$

Metamath Proof Explorer