Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΎ β HL β§ π β π»)) |
2 | | simp3l 1198 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β πΉ β π) |
3 | | cdlemg8.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | cdlemg8.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | cdlemg8.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
6 | | cdlemg10.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
7 | 3, 4, 5, 6 | trlle 39568 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β€ π) |
8 | 1, 2, 7 | syl2anc 583 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (π
βπΉ) β€ π) |
9 | 8 | biantrud 531 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β€ ((πΊβπ) β¨ (πΊβπ)) β ((π
βπΉ) β€ ((πΊβπ) β¨ (πΊβπ)) β§ (π
βπΉ) β€ π))) |
10 | | simp1l 1194 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β πΎ β HL) |
11 | 10 | hllatd 38747 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β πΎ β Lat) |
12 | | eqid 2726 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
13 | 12, 4, 5, 6 | trlcl 39548 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β (BaseβπΎ)) |
14 | 1, 2, 13 | syl2anc 583 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (π
βπΉ) β (BaseβπΎ)) |
15 | | simp3r 1199 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β πΊ β π) |
16 | | simp2ll 1237 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β π β π΄) |
17 | | cdlemg8.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
18 | 3, 17, 4, 5 | ltrnat 39524 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
19 | 1, 15, 16, 18 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ) β π΄) |
20 | | simp2rl 1239 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β π β π΄) |
21 | 3, 17, 4, 5 | ltrnat 39524 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
22 | 1, 15, 20, 21 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ) β π΄) |
23 | | cdlemg8.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
24 | 12, 23, 17 | hlatjcl 38750 |
. . . 4
β’ ((πΎ β HL β§ (πΊβπ) β π΄ β§ (πΊβπ) β π΄) β ((πΊβπ) β¨ (πΊβπ)) β (BaseβπΎ)) |
25 | 10, 19, 22, 24 | syl3anc 1368 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((πΊβπ) β¨ (πΊβπ)) β (BaseβπΎ)) |
26 | | simp1r 1195 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β π β π») |
27 | 12, 4 | lhpbase 39382 |
. . . 4
β’ (π β π» β π β (BaseβπΎ)) |
28 | 26, 27 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β π β (BaseβπΎ)) |
29 | | cdlemg8.m |
. . . 4
β’ β§ =
(meetβπΎ) |
30 | 12, 3, 29 | latlem12 18431 |
. . 3
β’ ((πΎ β Lat β§ ((π
βπΉ) β (BaseβπΎ) β§ ((πΊβπ) β¨ (πΊβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π
βπΉ) β€ ((πΊβπ) β¨ (πΊβπ)) β§ (π
βπΉ) β€ π) β (π
βπΉ) β€ (((πΊβπ) β¨ (πΊβπ)) β§ π))) |
31 | 11, 14, 25, 28, 30 | syl13anc 1369 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (((π
βπΉ) β€ ((πΊβπ) β¨ (πΊβπ)) β§ (π
βπΉ) β€ π) β (π
βπΉ) β€ (((πΊβπ) β¨ (πΊβπ)) β§ π))) |
32 | 12, 23, 17 | hlatjcl 38750 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
33 | 10, 16, 20, 32 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (π β¨ π) β (BaseβπΎ)) |
34 | 12, 3, 29 | latlem12 18431 |
. . . 4
β’ ((πΎ β Lat β§ ((π
βπΉ) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π
βπΉ) β€ (π β¨ π) β§ (π
βπΉ) β€ π) β (π
βπΉ) β€ ((π β¨ π) β§ π))) |
35 | 11, 14, 33, 28, 34 | syl13anc 1369 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (((π
βπΉ) β€ (π β¨ π) β§ (π
βπΉ) β€ π) β (π
βπΉ) β€ ((π β¨ π) β§ π))) |
36 | 8 | biantrud 531 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β€ (π β¨ π) β ((π
βπΉ) β€ (π β¨ π) β§ (π
βπΉ) β€ π))) |
37 | 3, 23, 29, 17, 4, 5 | cdlemg10b 40019 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΊ β π) β (((πΊβπ) β¨ (πΊβπ)) β§ π) = ((π β¨ π) β§ π)) |
38 | 37 | 3adant3l 1177 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (((πΊβπ) β¨ (πΊβπ)) β§ π) = ((π β¨ π) β§ π)) |
39 | 38 | breq2d 5153 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β€ (((πΊβπ) β¨ (πΊβπ)) β§ π) β (π
βπΉ) β€ ((π β¨ π) β§ π))) |
40 | 35, 36, 39 | 3bitr4rd 312 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β€ (((πΊβπ) β¨ (πΊβπ)) β§ π) β (π
βπΉ) β€ (π β¨ π))) |
41 | 9, 31, 40 | 3bitrd 305 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β€ ((πΊβπ) β¨ (πΊβπ)) β (π
βπΉ) β€ (π β¨ π))) |