Theorem opltn0

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

	Ref	Expression
Hypotheses	opltne0.b	$$⊢B={\mathrm{Base}}_K$$
	opltne0.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	opltne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	opltn0	$$⊢\left(K\in \mathrm{OP}\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		opltne0.b	$$⊢B={\mathrm{Base}}_K$$
2		opltne0.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		opltne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		simpl	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to K\in \mathrm{OP}$$
5	1 3	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in B$$
6	5	adantr	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \underset{\dot{}}{0}\in B$$
7		simpr	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\in B$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9	8 2	pltval	$$⊢\left(K\in \mathrm{OP}\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{OP}\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	op0le	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \underset{\dot{}}{0}{\le }_{K}X$$
13	12	biantrurd	$$⊢\left(K\in \mathrm{OP}\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{OP}\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{OP}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$