| Step | Hyp | Ref
| Expression |
|---|
| 1 | | isdlat.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
| 2 | | isdlat.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
| 3 | | isdlat.m |
. . . 4
β’ β§ =
(meetβπΎ) |
| 4 | 1, 2, 3 | isdlat 18456 |
. . 3
β’ (πΎ β DLat β (πΎ β Lat β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
| 5 | 4 | simprbi 497 |
. 2
β’ (πΎ β DLat β
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
| 6 | | oveq1 7399 |
. . . 4
β’ (π₯ = π β (π₯ β§ (π¦ β¨ π§)) = (π β§ (π¦ β¨ π§))) |
| 7 | | oveq1 7399 |
. . . . 5
β’ (π₯ = π β (π₯ β§ π¦) = (π β§ π¦)) |
| 8 | | oveq1 7399 |
. . . . 5
β’ (π₯ = π β (π₯ β§ π§) = (π β§ π§)) |
| 9 | 7, 8 | oveq12d 7410 |
. . . 4
β’ (π₯ = π β ((π₯ β§ π¦) β¨ (π₯ β§ π§)) = ((π β§ π¦) β¨ (π β§ π§))) |
| 10 | 6, 9 | eqeq12d 2747 |
. . 3
β’ (π₯ = π β ((π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)) β (π β§ (π¦ β¨ π§)) = ((π β§ π¦) β¨ (π β§ π§)))) |
| 11 | | oveq1 7399 |
. . . . 5
β’ (π¦ = π β (π¦ β¨ π§) = (π β¨ π§)) |
| 12 | 11 | oveq2d 7408 |
. . . 4
β’ (π¦ = π β (π β§ (π¦ β¨ π§)) = (π β§ (π β¨ π§))) |
| 13 | | oveq2 7400 |
. . . . 5
β’ (π¦ = π β (π β§ π¦) = (π β§ π)) |
| 14 | 13 | oveq1d 7407 |
. . . 4
β’ (π¦ = π β ((π β§ π¦) β¨ (π β§ π§)) = ((π β§ π) β¨ (π β§ π§))) |
| 15 | 12, 14 | eqeq12d 2747 |
. . 3
β’ (π¦ = π β ((π β§ (π¦ β¨ π§)) = ((π β§ π¦) β¨ (π β§ π§)) β (π β§ (π β¨ π§)) = ((π β§ π) β¨ (π β§ π§)))) |
| 16 | | oveq2 7400 |
. . . . 5
β’ (π§ = π β (π β¨ π§) = (π β¨ π)) |
| 17 | 16 | oveq2d 7408 |
. . . 4
β’ (π§ = π β (π β§ (π β¨ π§)) = (π β§ (π β¨ π))) |
| 18 | | oveq2 7400 |
. . . . 5
β’ (π§ = π β (π β§ π§) = (π β§ π)) |
| 19 | 18 | oveq2d 7408 |
. . . 4
β’ (π§ = π β ((π β§ π) β¨ (π β§ π§)) = ((π β§ π) β¨ (π β§ π))) |
| 20 | 17, 19 | eqeq12d 2747 |
. . 3
β’ (π§ = π β ((π β§ (π β¨ π§)) = ((π β§ π) β¨ (π β§ π§)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π)))) |
| 21 | 10, 15, 20 | rspc3v 3622 |
. 2
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π)))) |
| 22 | 5, 21 | mpan9 507 |
1
β’ ((πΎ β DLat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) |
