Step | Hyp | Ref
| Expression |
1 | | cvrat4.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cvrat4.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | cvrat4.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | cvrat4.z |
. . 3
β’ 0 =
(0.βπΎ) |
5 | | cvrat4.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
6 | 1, 2, 3, 4, 5 | cvrat4 37952 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |
7 | | hllat 37871 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
8 | 7 | ad2antrr 725 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β πΎ β Lat) |
9 | | simplr3 1218 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β π΄) |
10 | 1, 5 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β π΅) |
12 | 1, 5 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
13 | 12 | adantl 483 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β π΅) |
14 | 1, 3 | latjcom 18341 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
15 | 8, 11, 13, 14 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
16 | 15 | breq2d 5118 |
. . . 4
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
17 | 16 | anbi2d 630 |
. . 3
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β ((π β€ π β§ π β€ (π β¨ π)) β (π β€ π β§ π β€ (π β¨ π)))) |
18 | 17 | rexbidva 3170 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (βπ β π΄ (π β€ π β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |
19 | 6, 18 | sylibd 238 |
1
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |