Theorem ltrnmw

Description: Property of lattice translation value. Remark below Lemma B in Crawley p. 112. TODO: Can this be used in more places? (Contributed by NM, 20-May-2012) (Proof shortened by OpenAI, 25-Mar-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ltrnmw.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ltrnmw.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3		ltrnmw.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		ltrnmw.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		ltrnmw.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		ltrnmw.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		simp1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8	1 4 5 6	ltrnel	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to \left(F\left(P\right)\in A\wedge \neg F\left(P\right)\underset{\dot{}}{\le }W\right)$$
9	1 2 3 4 5	lhpmat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\left(P\right)\in A\wedge \neg F\left(P\right)\underset{\dot{}}{\le }W\right)\right)\to F\left(P\right)\underset{\dot{}}{\wedge }W=\underset{\dot{}}{0}$$
10	7 8 9	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to F\left(P\right)\underset{\dot{}}{\wedge }W=\underset{\dot{}}{0}$$