Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β πΎ β HL) |
2 | | simp21l 1291 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β π΄) |
3 | | simp1r 1199 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β π») |
4 | | simp21 1207 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
5 | | simp22l 1293 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β π΄) |
6 | | simp31 1210 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β π) |
7 | | cdlemg12.l |
. . . 4
β’ β€ =
(leβπΎ) |
8 | | cdlemg12.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
9 | | cdlemg12.m |
. . . 4
β’ β§ =
(meetβπΎ) |
10 | | cdlemg12.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
11 | | cdlemg12.h |
. . . 4
β’ π» = (LHypβπΎ) |
12 | | cdlemg18b.u |
. . . 4
β’ π = ((π β¨ π) β§ π) |
13 | 7, 8, 9, 10, 11, 12 | cdleme0a 38703 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) |
14 | 1, 3, 4, 5, 6, 13 | syl212anc 1381 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β π΄) |
15 | | simp1 1137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (πΎ β HL β§ π β π»)) |
16 | | simp23 1209 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β πΉ β π) |
17 | | cdlemg12.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
18 | 7, 10, 11, 17 | ltrnat 38632 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
19 | 15, 16, 5, 18 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (πΉβπ) β π΄) |
20 | 7, 10, 11, 17 | ltrnat 38632 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
21 | 15, 16, 2, 20 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (πΉβπ) β π΄) |
22 | | cdlemg12b.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
23 | 7, 8, 9, 10, 11, 17, 22, 12 | cdlemg18b 39171 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β Β¬ π β€ (π β¨ (πΉβπ))) |
24 | | simp32 1211 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (πΉβπ) β π) |
25 | 24 | necomd 3000 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β (πΉβπ)) |
26 | 23, 25 | jca 513 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (Β¬ π β€ (π β¨ (πΉβπ)) β§ π β (πΉβπ))) |
27 | | simp33 1212 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π)) |
28 | 7, 8, 9, 10, 11, 17, 22 | cdlemg18a 39170 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ πΉ β π) β§ (π β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) |
29 | 15, 2, 5, 16, 6, 27, 28 | syl132anc 1389 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) |
30 | 7, 8, 10 | hlatlej2 37867 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
31 | 1, 2, 5, 30 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β€ (π β¨ π)) |
32 | 7, 8, 9, 10, 11, 12 | cdleme0cp 38706 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
33 | 1, 3, 4, 5, 32 | syl22anc 838 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β¨ π) = (π β¨ π)) |
34 | 31, 33 | breqtrrd 5138 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β π β€ (π β¨ π)) |
35 | 7, 8, 10 | hlatlej2 37867 |
. . . . 5
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ (πΉβπ) β π΄) β (πΉβπ) β€ ((πΉβπ) β¨ (πΉβπ))) |
36 | 1, 19, 21, 35 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (πΉβπ) β€ ((πΉβπ) β¨ (πΉβπ))) |
37 | | simp22 1208 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
38 | 11, 17, 7, 8, 10, 9,
12 | cdlemg2kq 39094 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) |
39 | 15, 4, 37, 16, 38 | syl121anc 1376 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) |
40 | 8, 10 | hlatjcom 37859 |
. . . . . 6
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ (πΉβπ) β π΄) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
41 | 1, 21, 19, 40 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
42 | 8, 10 | hlatjcom 37859 |
. . . . . 6
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ π β π΄) β ((πΉβπ) β¨ π) = (π β¨ (πΉβπ))) |
43 | 1, 19, 14, 42 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((πΉβπ) β¨ π) = (π β¨ (πΉβπ))) |
44 | 39, 41, 43 | 3eqtr3d 2785 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((πΉβπ) β¨ (πΉβπ)) = (π β¨ (πΉβπ))) |
45 | 36, 44 | breqtrd 5136 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (πΉβπ) β€ (π β¨ (πΉβπ))) |
46 | 34, 45 | jca 513 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β€ (π β¨ π) β§ (πΉβπ) β€ (π β¨ (πΉβπ)))) |
47 | 7, 8, 9, 10 | ps-2c 38020 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ((πΉβπ) β π΄ β§ π β π΄ β§ (πΉβπ) β π΄) β§ ((Β¬ π β€ (π β¨ (πΉβπ)) β§ π β (πΉβπ)) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)) β§ (π β€ (π β¨ π) β§ (πΉβπ) β€ (π β¨ (πΉβπ))))) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄) |
48 | 1, 2, 14, 19, 5, 21, 26, 29, 46, 47 | syl333anc 1403 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄) |