Metamath Proof Explorer


Theorem cdleme32e

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

Ref Expression
Hypotheses cdleme32.b B=BaseK
cdleme32.l ˙=K
cdleme32.j ˙=joinK
cdleme32.m ˙=meetK
cdleme32.a A=AtomsK
cdleme32.h H=LHypK
cdleme32.u U=P˙Q˙W
cdleme32.c C=s˙U˙Q˙P˙s˙W
cdleme32.d D=t˙U˙Q˙P˙t˙W
cdleme32.e E=P˙Q˙D˙s˙t˙W
cdleme32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
cdleme32.n N=ifs˙P˙QIC
cdleme32.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
cdleme32.f F=xBifPQ¬x˙WOx
Assertion cdleme32e KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YFX˙FY

Proof

Step Hyp Ref Expression
1 cdleme32.b B=BaseK
2 cdleme32.l ˙=K
3 cdleme32.j ˙=joinK
4 cdleme32.m ˙=meetK
5 cdleme32.a A=AtomsK
6 cdleme32.h H=LHypK
7 cdleme32.u U=P˙Q˙W
8 cdleme32.c C=s˙U˙Q˙P˙s˙W
9 cdleme32.d D=t˙U˙Q˙P˙t˙W
10 cdleme32.e E=P˙Q˙D˙s˙t˙W
11 cdleme32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
12 cdleme32.n N=ifs˙P˙QIC
13 cdleme32.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
14 cdleme32.f F=xBifPQ¬x˙WOx
15 simp23l KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YPQ
16 15 pm2.24d KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙Y¬PQX˙N˙Y˙W
17 simp11l KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YKHL
18 17 hllatd KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YKLat
19 simp21l KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YXB
20 simp11r KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YWH
21 1 6 lhpbase WHWB
22 20 21 syl KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YWB
23 1 2 4 latleeqm1 KLatXBWBX˙WX˙W=X
24 18 19 22 23 syl3anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙WX˙W=X
25 1 4 latmcl KLatXBWBX˙WB
26 18 19 22 25 syl3anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙WB
27 simp21r KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YYB
28 1 4 latmcl KLatYBWBY˙WB
29 18 27 22 28 syl3anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YY˙WB
30 simp11 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YKHLWH
31 simp12 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YPA¬P˙W
32 simp13 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YQA¬Q˙W
33 simp31 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YsA¬s˙W
34 1 2 3 4 5 6 7 8 9 10 11 12 cdleme27cl KHLWHPA¬P˙WQA¬Q˙WsA¬s˙WPQNB
35 30 31 32 33 15 34 syl122anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YNB
36 1 3 latjcl KLatNBY˙WBN˙Y˙WB
37 18 35 29 36 syl3anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YN˙Y˙WB
38 simp33 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙Y
39 1 2 4 latmlem1 KLatXBYBWBX˙YX˙W˙Y˙W
40 18 19 27 22 39 syl13anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙YX˙W˙Y˙W
41 38 40 mpd KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙W˙Y˙W
42 1 2 3 latlej2 KLatNBY˙WBY˙W˙N˙Y˙W
43 18 35 29 42 syl3anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YY˙W˙N˙Y˙W
44 1 2 18 26 29 37 41 43 lattrd KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙W˙N˙Y˙W
45 breq1 X˙W=XX˙W˙N˙Y˙WX˙N˙Y˙W
46 44 45 syl5ibcom KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙W=XX˙N˙Y˙W
47 24 46 sylbid KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙WX˙N˙Y˙W
48 simp22 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙Y¬PQ¬X˙W
49 pm4.53 ¬PQ¬X˙W¬PQX˙W
50 48 49 sylib KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙Y¬PQX˙W
51 16 47 50 mpjaod KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YX˙N˙Y˙W
52 14 cdleme31fv2 XB¬PQ¬X˙WFX=X
53 19 48 52 syl2anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YFX=X
54 simp1 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YKHLWHPA¬P˙WQA¬Q˙W
55 simp23 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YPQ¬Y˙W
56 simp32 KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙Ys˙Y˙W=Y
57 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32a KHLWHPA¬P˙WQA¬Q˙WYBPQ¬Y˙WsA¬s˙Ws˙Y˙W=YFY=N˙Y˙W
58 54 27 55 33 56 57 syl122anc KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YFY=N˙Y˙W
59 51 53 58 3brtr4d KHLWHPA¬P˙WQA¬Q˙WXBYB¬PQ¬X˙WPQ¬Y˙WsA¬s˙Ws˙Y˙W=YX˙YFX˙FY