Theorem lhpn0

Description: A co-atom is nonzero. TODO: is this needed? (Contributed by NM, 26-Apr-2013)

	Ref	Expression
Hypotheses	lhpne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	lhpne0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpn0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lhpne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
2		lhpne0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		eqid	$$⊢{<}_K={<}_K$$
4	3 1 2	lhp0lt	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{0}{<}_{K}W$$
5		simpl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to K\in \mathrm{HL}$$
6		hlop	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OP}$$
7		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
8	7 1	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
9	6 8	syl	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
10	9	adantr	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
11		simpr	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W\in H$$
12	3	pltne	$$⊢\left(K\in \mathrm{HL}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\wedge W\in H\right)\to \left(\underset{\dot{}}{0}{<}_{K}W\to \underset{\dot{}}{0}\ne W\right)$$
13	5 10 11 12	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left(\underset{\dot{}}{0}{<}_{K}W\to \underset{\dot{}}{0}\ne W\right)$$
14	4 13	mpd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{0}\ne W$$
15	14	necomd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W\ne \underset{\dot{}}{0}$$