Step | Hyp | Ref
| Expression |
1 | | cdlemf1.l |
. . . 4
β’ β€ =
(leβπΎ) |
2 | | cdlemf1.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
3 | | cdlemf1.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | 1, 2, 3 | lhpexnle 38498 |
. . 3
β’ ((πΎ β HL β§ π β π») β βπ β π΄ Β¬ π β€ π) |
5 | 4 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π΄ Β¬ π β€ π) |
6 | | cdlemf1.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
7 | 1, 6, 2, 3 | cdlemf1 39053 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) |
8 | | simpr1r 1232 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β Β¬ π β€ π) |
9 | | simpr32 1265 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β Β¬ π β€ π) |
10 | | simpr33 1266 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β€ (π β¨ π)) |
11 | | simplrr 777 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β€ π) |
12 | | hllat 37854 |
. . . . . . . . . . . . . 14
β’ (πΎ β HL β πΎ β Lat) |
13 | 12 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β πΎ β Lat) |
14 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β π΄) |
15 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(BaseβπΎ) =
(BaseβπΎ) |
16 | 15, 2 | atbase 37780 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π β (BaseβπΎ)) |
17 | 14, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β (BaseβπΎ)) |
18 | | simplll 774 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β πΎ β HL) |
19 | | simpr1l 1231 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β π΄) |
20 | | simpr2 1196 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β π΄) |
21 | 15, 6, 2 | hlatjcl 37858 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
22 | 18, 19, 20, 21 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β (π β¨ π) β (BaseβπΎ)) |
23 | 15, 3 | lhpbase 38490 |
. . . . . . . . . . . . . 14
β’ (π β π» β π β (BaseβπΎ)) |
24 | 23 | ad3antlr 730 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β (BaseβπΎ)) |
25 | | cdlemf2.m |
. . . . . . . . . . . . . 14
β’ β§ =
(meetβπΎ) |
26 | 15, 1, 25 | latlem12 18362 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β€ (π β¨ π) β§ π β€ π) β π β€ ((π β¨ π) β§ π))) |
27 | 13, 17, 22, 24, 26 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β ((π β€ (π β¨ π) β§ π β€ π) β π β€ ((π β¨ π) β§ π))) |
28 | 10, 11, 27 | mpbi2and 711 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β€ ((π β¨ π) β§ π)) |
29 | | hlatl 37851 |
. . . . . . . . . . . . 13
β’ (πΎ β HL β πΎ β AtLat) |
30 | 29 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β πΎ β AtLat) |
31 | | simpll 766 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
32 | | simpr31 1264 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π β π) |
33 | 1, 6, 25, 2, 3 | lhpat 38535 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β ((π β¨ π) β§ π) β π΄) |
34 | 31, 19, 8, 20, 32, 33 | syl122anc 1380 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β ((π β¨ π) β§ π) β π΄) |
35 | 1, 2 | atcmp 37802 |
. . . . . . . . . . . 12
β’ ((πΎ β AtLat β§ π β π΄ β§ ((π β¨ π) β§ π) β π΄) β (π β€ ((π β¨ π) β§ π) β π = ((π β¨ π) β§ π))) |
36 | 30, 14, 34, 35 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β (π β€ ((π β¨ π) β§ π) β π = ((π β¨ π) β§ π))) |
37 | 28, 36 | mpbid 231 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β π = ((π β¨ π) β§ π)) |
38 | 8, 9, 37 | jca31 516 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)))) β ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π))) |
39 | 38 | 3exp2 1355 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β ((π β π΄ β§ Β¬ π β€ π) β (π β π΄ β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π)))))) |
40 | 39 | 3impia 1118 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β π΄ β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π))))) |
41 | 40 | reximdvai 3163 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π)))) |
42 | 7, 41 | mpd 15 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π))) |
43 | 42 | 3expia 1122 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β ((π β π΄ β§ Β¬ π β€ π) β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π)))) |
44 | 43 | expd 417 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β (π β π΄ β (Β¬ π β€ π β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π))))) |
45 | 44 | reximdvai 3163 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β (βπ β π΄ Β¬ π β€ π β βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π)))) |
46 | 5, 45 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π))) |