Theorem atn0

Description: An atom is not zero. ( atne0 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	atne0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atn0	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to P\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		atne0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
2		atne0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5	3 4 1 2	isat3	$$⊢K\in \mathrm{AtLat}\to \left(P\in A\leftrightarrow \left(P\in {\mathrm{Base}}_K\wedge P\ne \underset{\dot{}}{0}\wedge \forall x\in {\mathrm{Base}}_K\left(x{\le }_{K}P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)$$
6		simp2	$$⊢\left(P\in {\mathrm{Base}}_K\wedge P\ne \underset{\dot{}}{0}\wedge \forall x\in {\mathrm{Base}}_K\left(x{\le }_{K}P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\to P\ne \underset{\dot{}}{0}$$
7	5 6	syl6bi	$$⊢K\in \mathrm{AtLat}\to \left(P\in A\to P\ne \underset{\dot{}}{0}\right)$$
8	7	imp	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to P\ne \underset{\dot{}}{0}$$