Step | Hyp | Ref
| Expression |
1 | | ishlat.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | ishlat.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | ishlat.s |
. . 3
β’ < =
(ltβπΎ) |
4 | | ishlat.j |
. . 3
β’ β¨ =
(joinβπΎ) |
5 | | ishlat.z |
. . 3
β’ 0 =
(0.βπΎ) |
6 | | ishlat.u |
. . 3
β’ 1 =
(1.βπΎ) |
7 | | ishlat.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
8 | 1, 2, 3, 4, 5, 6, 7 | ishlat1 37860 |
. 2
β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§
(βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
9 | | simpll3 1215 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β§ π§ β π΄) β πΎ β CvLat) |
10 | | simplrl 776 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β§ π§ β π΄) β π₯ β π΄) |
11 | | simplrr 777 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β§ π§ β π΄) β π¦ β π΄) |
12 | | simpr 486 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β§ π§ β π΄) β π§ β π΄) |
13 | 7, 2, 4 | cvlsupr3 37852 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π₯ β π΄ β§ π¦ β π΄ β§ π§ β π΄)) β ((π₯ β¨ π§) = (π¦ β¨ π§) β (π₯ β π¦ β (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
14 | 9, 10, 11, 12, 13 | syl13anc 1373 |
. . . . . . 7
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β§ π§ β π΄) β ((π₯ β¨ π§) = (π¦ β¨ π§) β (π₯ β π¦ β (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
15 | 14 | rexbidva 3170 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§) β βπ§ β π΄ (π₯ β π¦ β (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
16 | | ne0i 4295 |
. . . . . . . 8
β’ (π₯ β π΄ β π΄ β β
) |
17 | 16 | ad2antrl 727 |
. . . . . . 7
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β π΄ β β
) |
18 | | r19.37zv 4460 |
. . . . . . 7
β’ (π΄ β β
β
(βπ§ β π΄ (π₯ β π¦ β (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
19 | 17, 18 | syl 17 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β (βπ§ β π΄ (π₯ β π¦ β (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
20 | 15, 19 | bitr2d 280 |
. . . . 5
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§))) |
21 | 20 | 2ralbidva 3207 |
. . . 4
β’ ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β
(βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§))) |
22 | 21 | anbi1d 631 |
. . 3
β’ ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β
((βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))) β (βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
23 | 22 | pm5.32i 576 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§
(βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§
(βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
24 | 8, 23 | bitri 275 |
1
β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§
(βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ β¨ π§) = (π¦ β¨ π§) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |