Theorem ltrnnid

Description: If a lattice translation is not the identity, then there is an atom not under the fiducial co-atom W and not equal to its translation. (Contributed by NM, 24-May-2012)

	Ref	Expression
Hypotheses	ltrneq.b	$$⊢B={\mathrm{Base}}_K$$
	ltrneq.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ltrneq.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ltrneq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrneq.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrnnid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge F\ne {\mathrm{I}\upharpoonright }_B\right)\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge F\left(p\right)\ne p\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltrneq.b	$$⊢B={\mathrm{Base}}_K$$
2		ltrneq.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		ltrneq.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		ltrneq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		ltrneq.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		ralinexa	$$⊢\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to \neg F\left(p\right)\ne p\right)\leftrightarrow \neg \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge F\left(p\right)\ne p\right)$$
7		nne	$$⊢\neg F\left(p\right)\ne p\leftrightarrow F\left(p\right)=p$$
8	7	biimpi	$$⊢\neg F\left(p\right)\ne p\to F\left(p\right)=p$$
9	8	imim2i	$$⊢\left(\neg p\underset{\dot{}}{\le }W\to \neg F\left(p\right)\ne p\right)\to \left(\neg p\underset{\dot{}}{\le }W\to F\left(p\right)=p\right)$$
10	9	ralimi	$$⊢\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to \neg F\left(p\right)\ne p\right)\to \forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to F\left(p\right)=p\right)$$
11	6 10	sylbir	$$⊢\neg \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge F\left(p\right)\ne p\right)\to \forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to F\left(p\right)=p\right)$$
12	1 2 3 4 5	ltrnid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to F\left(p\right)=p\right)\leftrightarrow F={\mathrm{I}\upharpoonright }_B\right)$$
13	11 12	syl5ib	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(\neg \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge F\left(p\right)\ne p\right)\to F={\mathrm{I}\upharpoonright }_B\right)$$
14	13	necon1ad	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(F\ne {\mathrm{I}\upharpoonright }_B\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge F\left(p\right)\ne p\right)\right)$$
15	14	3impia	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge F\ne {\mathrm{I}\upharpoonright }_B\right)\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge F\left(p\right)\ne p\right)$$