Theorem atlltn0

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

	Ref	Expression
Hypotheses	atlltne0.b	$$⊢B={\mathrm{Base}}_K$$
	atlltne0.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	atlltne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	atlltn0	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		atlltne0.b	$$⊢B={\mathrm{Base}}_K$$
2		atlltne0.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		atlltne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		simpl	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to K\in \mathrm{AtLat}$$
5	1 3	atl0cl	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in B$$
6	5	adantr	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \underset{\dot{}}{0}\in B$$
7		simpr	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to X\in B$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9	8 2	pltval	$$⊢\left(K\in \mathrm{AtLat}\wedge \underset{\dot{}}{0}\in B\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{K}X\wedge \underset{\dot{}}{0}\ne X\right)\right)$$
10	4 6 7 9	syl3anc	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{K}X\wedge \underset{\dot{}}{0}\ne X\right)\right)$$
11		necom	$$⊢X\ne \underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}\ne X$$
12	1 8 3	atl0le	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \underset{\dot{}}{0}{\le }_{K}X$$
13	12	biantrurd	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\ne X\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{K}X\wedge \underset{\dot{}}{0}\ne X\right)\right)$$
14	11 13	syl5rbb	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \left(\left(\underset{\dot{}}{0}{\le }_{K}X\wedge \underset{\dot{}}{0}\ne X\right)\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$
15	10 14	bitrd	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$