Step | Hyp | Ref
| Expression |
1 | | iscvlat2.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | iscvlat2.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | iscvlat2.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | iscvlat2.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
5 | 1, 2, 3, 4 | iscvlat 37831 |
. 2
β’ (πΎ β CvLat β (πΎ β AtLat β§
βπ β π΄ βπ β π΄ βπ₯ β π΅ ((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) |
6 | | simpll 766 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β§ π₯ β π΅) β πΎ β AtLat) |
7 | | simplrl 776 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β§ π₯ β π΅) β π β π΄) |
8 | | simpr 486 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β§ π₯ β π΅) β π₯ β π΅) |
9 | | iscvlat2.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
10 | | iscvlat2.z |
. . . . . . . . 9
β’ 0 =
(0.βπΎ) |
11 | 1, 2, 9, 10, 4 | atnle 37825 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄ β§ π₯ β π΅) β (Β¬ π β€ π₯ β (π β§ π₯) = 0 )) |
12 | 6, 7, 8, 11 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β§ π₯ β π΅) β (Β¬ π β€ π₯ β (π β§ π₯) = 0 )) |
13 | 12 | anbi1d 631 |
. . . . . 6
β’ (((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β§ π₯ β π΅) β ((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β ((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)))) |
14 | 13 | imbi1d 342 |
. . . . 5
β’ (((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β§ π₯ β π΅) β (((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)) β (((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) |
15 | 14 | ralbidva 3169 |
. . . 4
β’ ((πΎ β AtLat β§ (π β π΄ β§ π β π΄)) β (βπ₯ β π΅ ((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)) β βπ₯ β π΅ (((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) |
16 | 15 | 2ralbidva 3207 |
. . 3
β’ (πΎ β AtLat β
(βπ β π΄ βπ β π΄ βπ₯ β π΅ ((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)) β βπ β π΄ βπ β π΄ βπ₯ β π΅ (((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) |
17 | 16 | pm5.32i 576 |
. 2
β’ ((πΎ β AtLat β§
βπ β π΄ βπ β π΄ βπ₯ β π΅ ((Β¬ π β€ π₯ β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π))) β (πΎ β AtLat β§ βπ β π΄ βπ β π΄ βπ₯ β π΅ (((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) |
18 | 5, 17 | bitri 275 |
1
β’ (πΎ β CvLat β (πΎ β AtLat β§
βπ β π΄ βπ β π΄ βπ₯ β π΅ (((π β§ π₯) = 0 β§ π β€ (π₯ β¨ π)) β π β€ (π₯ β¨ π)))) |