Metamath Proof Explorer


Theorem cdleme30a

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Feb-2013)

Ref Expression
Hypotheses cdleme30.b B=BaseK
cdleme30.l ˙=K
cdleme30.j ˙=joinK
cdleme30.m ˙=meetK
cdleme30.a A=AtomsK
cdleme30.h H=LHypK
Assertion cdleme30a KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W=Y

Proof

Step Hyp Ref Expression
1 cdleme30.b B=BaseK
2 cdleme30.l ˙=K
3 cdleme30.j ˙=joinK
4 cdleme30.m ˙=meetK
5 cdleme30.a A=AtomsK
6 cdleme30.h H=LHypK
7 simp1l KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YKHL
8 7 hllatd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YKLat
9 simp21 KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YsA
10 1 5 atbase sAsB
11 9 10 syl KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YsB
12 simp23 KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YYB
13 simp1r KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YWH
14 1 6 lhpbase WHWB
15 13 14 syl KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YWB
16 1 4 latmcl KLatYBWBY˙WB
17 8 12 15 16 syl3anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YY˙WB
18 simp22l KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YXB
19 1 3 latjass KLatsBY˙WBXBs˙Y˙W˙X=s˙Y˙W˙X
20 8 11 17 18 19 syl13anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W˙X=s˙Y˙W˙X
21 simp3l KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙X˙W=X
22 simp3r KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙Y
23 1 2 4 latmlem1 KLatXBYBWBX˙YX˙W˙Y˙W
24 8 18 12 15 23 syl13anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙YX˙W˙Y˙W
25 22 24 mpd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙W˙Y˙W
26 1 4 latmcl KLatXBWBX˙WB
27 8 18 15 26 syl3anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙WB
28 1 2 3 latjlej2 KLatX˙WBY˙WBsBX˙W˙Y˙Ws˙X˙W˙s˙Y˙W
29 8 27 17 11 28 syl13anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙W˙Y˙Ws˙X˙W˙s˙Y˙W
30 25 29 mpd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙X˙W˙s˙Y˙W
31 21 30 eqbrtrrd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙s˙Y˙W
32 1 3 latjcl KLatsBY˙WBs˙Y˙WB
33 8 11 17 32 syl3anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙WB
34 1 2 3 latleeqj2 KLatXBs˙Y˙WBX˙s˙Y˙Ws˙Y˙W˙X=s˙Y˙W
35 8 18 33 34 syl3anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YX˙s˙Y˙Ws˙Y˙W˙X=s˙Y˙W
36 31 35 mpbid KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W˙X=s˙Y˙W
37 simp1 KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YKHLWH
38 1 2 3 4 6 lhpmod2i2 KHLWHYBXBX˙YY˙W˙X=Y˙W˙X
39 37 12 18 22 38 syl121anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YY˙W˙X=Y˙W˙X
40 39 oveq2d KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W˙X=s˙Y˙W˙X
41 simp22 KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YXB¬X˙W
42 eqid 1.K=1.K
43 1 2 3 42 6 lhpj1 KHLWHXB¬X˙WW˙X=1.K
44 37 41 43 syl2anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YW˙X=1.K
45 44 oveq2d KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YY˙W˙X=Y˙1.K
46 hlol KHLKOL
47 7 46 syl KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YKOL
48 1 4 42 olm11 KOLYBY˙1.K=Y
49 47 12 48 syl2anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YY˙1.K=Y
50 45 49 eqtrd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙YY˙W˙X=Y
51 50 oveq2d KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W˙X=s˙Y
52 1 2 3 latlej1 KLatsBX˙WBs˙s˙X˙W
53 8 11 27 52 syl3anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙s˙X˙W
54 53 21 breqtrd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙X
55 1 2 8 11 18 12 54 22 lattrd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y
56 1 2 3 latleeqj1 KLatsBYBs˙Ys˙Y=Y
57 8 11 12 56 syl3anc KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Ys˙Y=Y
58 55 57 mpbid KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y=Y
59 40 51 58 3eqtrd KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W˙X=Y
60 20 36 59 3eqtr3d KHLWHsAXB¬X˙WYBs˙X˙W=XX˙Ys˙Y˙W=Y