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	|- .<_ = ( le ` K )
	ltrnmw.m	|- ./\ = ( meet ` K )
	ltrnmw.z	|- .0. = ( 0. ` K )
	ltrnmw.a	|- A = ( Atoms ` K )
	ltrnmw.h	|- H = ( LHyp ` K )
	ltrnmw.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrnmw	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) ./\ W ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		ltrnmw.l	|- .<_ = ( le ` K )
2		ltrnmw.m	|- ./\ = ( meet ` K )
3		ltrnmw.z	|- .0. = ( 0. ` K )
4		ltrnmw.a	|- A = ( Atoms ` K )
5		ltrnmw.h	|- H = ( LHyp ` K )
6		ltrnmw.t	|- T = ( ( LTrn ` K ) ` W )
7		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
8	1 4 5 6	ltrnel	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
9	1 2 3 4 5	lhpmat	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) ) -> ( ( F ` P ) ./\ W ) = .0. )
10	7 8 9	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) ./\ W ) = .0. )