Metamath Proof Explorer


Theorem cdleme50ltrn

Description: Part of proof of Lemma E in Crawley p. 113. F is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013)

Ref Expression
Hypotheses cdlemef50.b B=BaseK
cdlemef50.l ˙=K
cdlemef50.j ˙=joinK
cdlemef50.m ˙=meetK
cdlemef50.a A=AtomsK
cdlemef50.h H=LHypK
cdlemef50.u U=P˙Q˙W
cdlemef50.d D=t˙U˙Q˙P˙t˙W
cdlemefs50.e E=P˙Q˙D˙s˙t˙W
cdlemef50.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
cdleme50ltrn.t T=LTrnKW
Assertion cdleme50ltrn KHLWHPA¬P˙WQA¬Q˙WFT

Proof

Step Hyp Ref Expression
1 cdlemef50.b B=BaseK
2 cdlemef50.l ˙=K
3 cdlemef50.j ˙=joinK
4 cdlemef50.m ˙=meetK
5 cdlemef50.a A=AtomsK
6 cdlemef50.h H=LHypK
7 cdlemef50.u U=P˙Q˙W
8 cdlemef50.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs50.e E=P˙Q˙D˙s˙t˙W
10 cdlemef50.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 cdleme50ltrn.t T=LTrnKW
12 eqid LDilKW=LDilKW
13 1 2 3 4 5 6 7 8 9 10 12 cdleme50ldil KHLWHPA¬P˙WQA¬Q˙WFLDilKW
14 simp1 KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙WKHLWHPA¬P˙WQA¬Q˙W
15 simp2l KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙WdA
16 simp3l KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙W¬d˙W
17 1 2 3 4 5 6 7 8 9 10 cdleme50trn123 KHLWHPA¬P˙WQA¬Q˙WdA¬d˙Wd˙Fd˙W=U
18 14 15 16 17 syl12anc KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙Wd˙Fd˙W=U
19 simp2r KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙WeA
20 simp3r KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙W¬e˙W
21 1 2 3 4 5 6 7 8 9 10 cdleme50trn123 KHLWHPA¬P˙WQA¬Q˙WeA¬e˙We˙Fe˙W=U
22 14 19 20 21 syl12anc KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙We˙Fe˙W=U
23 18 22 eqtr4d KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙Wd˙Fd˙W=e˙Fe˙W
24 23 3exp KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙Wd˙Fd˙W=e˙Fe˙W
25 24 ralrimivv KHLWHPA¬P˙WQA¬Q˙WdAeA¬d˙W¬e˙Wd˙Fd˙W=e˙Fe˙W
26 2 3 4 5 6 12 11 isltrn KHLWHFTFLDilKWdAeA¬d˙W¬e˙Wd˙Fd˙W=e˙Fe˙W
27 26 3ad2ant1 KHLWHPA¬P˙WQA¬Q˙WFTFLDilKWdAeA¬d˙W¬e˙Wd˙Fd˙W=e˙Fe˙W
28 13 25 27 mpbir2and KHLWHPA¬P˙WQA¬Q˙WFT