Metamath Proof Explorer


Theorem cdlemg7fvbwN

Description: Properties of a translation of an element not under W . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw ? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg4.l ˙=K
cdlemg4.a A=AtomsK
cdlemg4.h H=LHypK
cdlemg4.t T=LTrnKW
cdlemg4.b B=BaseK
Assertion cdlemg7fvbwN KHLWHXB¬X˙WFTFXB¬FX˙W

Proof

Step Hyp Ref Expression
1 cdlemg4.l ˙=K
2 cdlemg4.a A=AtomsK
3 cdlemg4.h H=LHypK
4 cdlemg4.t T=LTrnKW
5 cdlemg4.b B=BaseK
6 eqid joinK=joinK
7 eqid meetK=meetK
8 5 1 6 7 2 3 lhpmcvr2 KHLWHXB¬X˙WrA¬r˙WrjoinKXmeetKW=X
9 8 3adant3 KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=X
10 simp11 KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XKHLWH
11 simp2 KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XrA
12 simp3l KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=X¬r˙W
13 11 12 jca KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XrA¬r˙W
14 simp12 KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XXB¬X˙W
15 simp13 KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFT
16 simp3r KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XrjoinKXmeetKW=X
17 3 4 1 6 2 7 5 cdlemg2fv KHLWHrA¬r˙WXB¬X˙WFTrjoinKXmeetKW=XFX=FrjoinKXmeetKW
18 10 13 14 15 16 17 syl122anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFX=FrjoinKXmeetKW
19 simp11l KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XKHL
20 19 hllatd KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XKLat
21 1 2 3 4 ltrnel KHLWHFTrA¬r˙WFrA¬Fr˙W
22 21 simpld KHLWHFTrA¬r˙WFrA
23 10 15 13 22 syl3anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFrA
24 5 2 atbase FrAFrB
25 23 24 syl KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFrB
26 simp12l KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XXB
27 simp11r KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XWH
28 5 3 lhpbase WHWB
29 27 28 syl KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XWB
30 5 7 latmcl KLatXBWBXmeetKWB
31 20 26 29 30 syl3anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XXmeetKWB
32 5 6 latjcl KLatFrBXmeetKWBFrjoinKXmeetKWB
33 20 25 31 32 syl3anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFrjoinKXmeetKWB
34 18 33 eqeltrd KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFXB
35 21 simprd KHLWHFTrA¬r˙W¬Fr˙W
36 10 15 13 35 syl3anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=X¬Fr˙W
37 5 1 6 latlej1 KLatFrBXmeetKWBFr˙FrjoinKXmeetKW
38 20 25 31 37 syl3anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFr˙FrjoinKXmeetKW
39 5 1 lattr KLatFrBFrjoinKXmeetKWBWBFr˙FrjoinKXmeetKWFrjoinKXmeetKW˙WFr˙W
40 20 25 33 29 39 syl13anc KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFr˙FrjoinKXmeetKWFrjoinKXmeetKW˙WFr˙W
41 38 40 mpand KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFrjoinKXmeetKW˙WFr˙W
42 36 41 mtod KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=X¬FrjoinKXmeetKW˙W
43 18 breq1d KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFX˙WFrjoinKXmeetKW˙W
44 42 43 mtbird KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=X¬FX˙W
45 34 44 jca KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFXB¬FX˙W
46 45 rexlimdv3a KHLWHXB¬X˙WFTrA¬r˙WrjoinKXmeetKW=XFXB¬FX˙W
47 9 46 mpd KHLWHXB¬X˙WFTFXB¬FX˙W