Step | Hyp | Ref
| Expression |
1 | | simp33 1212 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) |
2 | | simp3r 1203 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β€ (π β¨ (πΉβπ))) |
3 | | simp1l 1198 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β πΎ β HL) |
4 | | simp1r 1199 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β π») |
5 | | simp21 1207 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β π΄ β§ Β¬ π β€ π)) |
6 | | simp22l 1293 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β π΄) |
7 | | simp3l1 1279 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β π) |
8 | | cdlemg12.l |
. . . . . . . . . . . . 13
β’ β€ =
(leβπΎ) |
9 | | cdlemg12.j |
. . . . . . . . . . . . 13
β’ β¨ =
(joinβπΎ) |
10 | | cdlemg12.m |
. . . . . . . . . . . . 13
β’ β§ =
(meetβπΎ) |
11 | | cdlemg12.a |
. . . . . . . . . . . . 13
β’ π΄ = (AtomsβπΎ) |
12 | | cdlemg12.h |
. . . . . . . . . . . . 13
β’ π» = (LHypβπΎ) |
13 | | cdlemg18b.u |
. . . . . . . . . . . . 13
β’ π = ((π β¨ π) β§ π) |
14 | 8, 9, 10, 11, 12, 13 | cdleme0a 38703 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) |
15 | 3, 4, 5, 6, 7, 14 | syl212anc 1381 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β π΄) |
16 | | simp1 1137 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (πΎ β HL β§ π β π»)) |
17 | | simp23 1209 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β πΉ β π) |
18 | | cdlemg12.t |
. . . . . . . . . . . . 13
β’ π = ((LTrnβπΎ)βπ) |
19 | 8, 11, 12, 18 | ltrnat 38632 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
20 | 16, 17, 6, 19 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (πΉβπ) β π΄) |
21 | 8, 9, 11 | hlatlej1 37866 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβπ) β π΄) β π β€ (π β¨ (πΉβπ))) |
22 | 3, 15, 20, 21 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β€ (π β¨ (πΉβπ))) |
23 | 3 | hllatd 37855 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β πΎ β Lat) |
24 | | simp21l 1291 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β π΄) |
25 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(BaseβπΎ) =
(BaseβπΎ) |
26 | 25, 11 | atbase 37780 |
. . . . . . . . . . . 12
β’ (π β π΄ β π β (BaseβπΎ)) |
27 | 24, 26 | syl 17 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β (BaseβπΎ)) |
28 | 25, 11 | atbase 37780 |
. . . . . . . . . . . 12
β’ (π β π΄ β π β (BaseβπΎ)) |
29 | 15, 28 | syl 17 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β π β (BaseβπΎ)) |
30 | 25, 9, 11 | hlatjcl 37858 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβπ) β π΄) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
31 | 3, 15, 20, 30 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
32 | 25, 8, 9 | latjle12 18346 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β¨ (πΉβπ)) β (BaseβπΎ))) β ((π β€ (π β¨ (πΉβπ)) β§ π β€ (π β¨ (πΉβπ))) β (π β¨ π) β€ (π β¨ (πΉβπ)))) |
33 | 23, 27, 29, 31, 32 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β ((π β€ (π β¨ (πΉβπ)) β§ π β€ (π β¨ (πΉβπ))) β (π β¨ π) β€ (π β¨ (πΉβπ)))) |
34 | 2, 22, 33 | mpbi2and 711 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β¨ π) β€ (π β¨ (πΉβπ))) |
35 | 8, 9, 10, 11, 12, 13 | cdleme0cp 38706 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
36 | 3, 4, 5, 6, 35 | syl22anc 838 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β¨ π) = (π β¨ π)) |
37 | | simp22 1208 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β π΄ β§ Β¬ π β€ π)) |
38 | 12, 18, 8, 9, 11, 10, 13 | cdlemg2kq 39094 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) |
39 | 16, 5, 37, 17, 38 | syl121anc 1376 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) |
40 | 9, 11 | hlatjcom 37859 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ π β π΄) β ((πΉβπ) β¨ π) = (π β¨ (πΉβπ))) |
41 | 3, 20, 15, 40 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β ((πΉβπ) β¨ π) = (π β¨ (πΉβπ))) |
42 | 39, 41 | eqtr2d 2778 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
43 | 34, 36, 42 | 3brtr3d 5141 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β¨ π) β€ ((πΉβπ) β¨ (πΉβπ))) |
44 | 8, 11, 12, 18 | ltrnat 38632 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
45 | 16, 17, 24, 44 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (πΉβπ) β π΄) |
46 | 8, 9, 11 | ps-1 37969 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ ((πΉβπ) β π΄ β§ (πΉβπ) β π΄)) β ((π β¨ π) β€ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π) = ((πΉβπ) β¨ (πΉβπ)))) |
47 | 3, 24, 6, 7, 45, 20, 46 | syl132anc 1389 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β ((π β¨ π) β€ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π) = ((πΉβπ) β¨ (πΉβπ)))) |
48 | 43, 47 | mpbid 231 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β (π β¨ π) = ((πΉβπ) β¨ (πΉβπ))) |
49 | 9, 11 | hlatjcom 37859 |
. . . . . . . 8
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ (πΉβπ) β π΄) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
50 | 3, 45, 20, 49 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
51 | 48, 50 | eqtr2d 2778 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ)))) β ((πΉβπ) β¨ (πΉβπ)) = (π β¨ π)) |
52 | 51 | 3exp 1120 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β (((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β§ π β€ (π β¨ (πΉβπ))) β ((πΉβπ) β¨ (πΉβπ)) = (π β¨ π)))) |
53 | 52 | exp4a 433 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β ((π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) β (π β€ (π β¨ (πΉβπ)) β ((πΉβπ) β¨ (πΉβπ)) = (π β¨ π))))) |
54 | 53 | 3imp 1112 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β€ (π β¨ (πΉβπ)) β ((πΉβπ) β¨ (πΉβπ)) = (π β¨ π))) |
55 | 54 | necon3ad 2957 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (((πΉβπ) β¨ (πΉβπ)) β (π β¨ π) β Β¬ π β€ (π β¨ (πΉβπ)))) |
56 | 1, 55 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β Β¬ π β€ (π β¨ (πΉβπ))) |