Theorem ltrnatneq

Description: If any atom (under W ) is not equal to its translation, so is any other atom. TODO: -. P .<_ W isn't needed to prove this. Will removing it shorten (and not lengthen) proofs using it? (Contributed by NM, 6-May-2013)

	Ref	Expression
Hypotheses	ltrn2eq.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ltrn2eq.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ltrn2eq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrn2eq.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrnatneq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge F\left(P\right)\ne P\right)\to F\left(Q\right)\ne Q$$

Proof

Step	Hyp	Ref	Expression
1		ltrn2eq.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ltrn2eq.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		ltrn2eq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		ltrn2eq.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
5	1 2 3 4	ltrn2ateq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\right)\to \left(F\left(P\right)=P\leftrightarrow F\left(Q\right)=Q\right)$$
6	5	necon3bid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\right)\to \left(F\left(P\right)\ne P\leftrightarrow F\left(Q\right)\ne Q\right)$$
7	6	biimp3a	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge F\left(P\right)\ne P\right)\to F\left(Q\right)\ne Q$$