Metamath Proof Explorer


Theorem cdleme21c

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 28-Nov-2012)

Ref Expression
Hypotheses cdleme21.l ˙=K
cdleme21.j ˙=joinK
cdleme21.m ˙=meetK
cdleme21.a A=AtomsK
cdleme21.h H=LHypK
cdleme21.u U=P˙Q˙W
Assertion cdleme21c KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙z¬U˙S˙z

Proof

Step Hyp Ref Expression
1 cdleme21.l ˙=K
2 cdleme21.j ˙=joinK
3 cdleme21.m ˙=meetK
4 cdleme21.a A=AtomsK
5 cdleme21.h H=LHypK
6 cdleme21.u U=P˙Q˙W
7 simp23 KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙z¬S˙P˙Q
8 simp11l KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zKHL
9 hlcvl KHLKCvLat
10 8 9 syl KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zKCvLat
11 simp12l KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zPA
12 simp21 KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zSA
13 simp3l KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zzA
14 simp13 KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zQA
15 1 2 4 atnlej1 KHLSAPAQA¬S˙P˙QSP
16 15 necomd KHLSAPAQA¬S˙P˙QPS
17 8 12 11 14 7 16 syl131anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zPS
18 simp3r KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙z=S˙z
19 4 2 cvlsupr7 KCvLatPASAzAPSP˙z=S˙zP˙S=z˙S
20 10 11 12 13 17 18 19 syl132anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙S=z˙S
21 2 4 hlatjcom KHLzASAz˙S=S˙z
22 8 13 12 21 syl3anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zz˙S=S˙z
23 20 22 eqtrd KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙S=S˙z
24 23 breq2d KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zU˙P˙SU˙S˙z
25 simp11r KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zWH
26 simp12r KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙z¬P˙W
27 simp22 KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zPQ
28 1 2 3 4 5 6 cdleme0a KHLWHPA¬P˙WQAPQUA
29 8 25 11 26 14 27 28 syl222anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zUA
30 8 hllatd KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zKLat
31 eqid BaseK=BaseK
32 31 2 4 hlatjcl KHLPAQAP˙QBaseK
33 8 11 14 32 syl3anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙QBaseK
34 31 5 lhpbase WHWBaseK
35 25 34 syl KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zWBaseK
36 31 1 3 latmle2 KLatP˙QBaseKWBaseKP˙Q˙W˙W
37 30 33 35 36 syl3anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙Q˙W˙W
38 6 37 eqbrtrid KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zU˙W
39 nbrne2 U˙W¬P˙WUP
40 38 26 39 syl2anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zUP
41 1 2 4 cvlatexch1 KCvLatUASAPAUPU˙P˙SS˙P˙U
42 10 29 12 11 40 41 syl131anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zU˙P˙SS˙P˙U
43 1 2 4 hlatlej1 KHLPAQAP˙P˙Q
44 8 11 14 43 syl3anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙P˙Q
45 1 2 3 4 5 6 cdlemeulpq KHLWHPAQAU˙P˙Q
46 8 25 11 14 45 syl22anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zU˙P˙Q
47 31 4 atbase PAPBaseK
48 11 47 syl KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zPBaseK
49 31 4 atbase UAUBaseK
50 29 49 syl KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zUBaseK
51 31 1 2 latjle12 KLatPBaseKUBaseKP˙QBaseKP˙P˙QU˙P˙QP˙U˙P˙Q
52 30 48 50 33 51 syl13anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙P˙QU˙P˙QP˙U˙P˙Q
53 44 46 52 mpbi2and KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙U˙P˙Q
54 31 4 atbase SASBaseK
55 12 54 syl KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zSBaseK
56 31 2 4 hlatjcl KHLPAUAP˙UBaseK
57 8 11 29 56 syl3anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zP˙UBaseK
58 31 1 lattr KLatSBaseKP˙UBaseKP˙QBaseKS˙P˙UP˙U˙P˙QS˙P˙Q
59 30 55 57 33 58 syl13anc KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zS˙P˙UP˙U˙P˙QS˙P˙Q
60 53 59 mpan2d KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zS˙P˙US˙P˙Q
61 42 60 syld KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zU˙P˙SS˙P˙Q
62 24 61 sylbird KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙zU˙S˙zS˙P˙Q
63 7 62 mtod KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙z¬U˙S˙z