Step | Hyp | Ref
| Expression |
1 | | hllat 38325 |
. . . . 5
β’ (πΎ β HL β πΎ β Lat) |
2 | 1 | 3ad2ant1 1133 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β πΎ β Lat) |
3 | | simp21 1206 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β π β π΄) |
4 | | simp1 1136 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β πΎ β HL) |
5 | | simp22 1207 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β π β π΄) |
6 | | simp23 1208 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β π β π΄) |
7 | | paddasslem.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
8 | | paddasslem.p |
. . . . . 6
β’ + =
(+πβπΎ) |
9 | 7, 8 | paddssat 38777 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π + π) β π΄) |
10 | 4, 5, 6, 9 | syl3anc 1371 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β (π + π) β π΄) |
11 | | simp3l 1201 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β (π β β
β§ (π + π) β β
)) |
12 | | paddasslem.l |
. . . . 5
β’ β€ =
(leβπΎ) |
13 | | paddasslem.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
14 | 12, 13, 7, 8 | elpaddn0 38763 |
. . . 4
β’ (((πΎ β Lat β§ π β π΄ β§ (π + π) β π΄) β§ (π β β
β§ (π + π) β β
)) β (π β (π + (π + π)) β (π β π΄ β§ βπ₯ β π βπ β (π + π)π β€ (π₯ β¨ π)))) |
15 | 2, 3, 10, 11, 14 | syl31anc 1373 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β (π β (π + (π + π)) β (π β π΄ β§ βπ₯ β π βπ β (π + π)π β€ (π₯ β¨ π)))) |
16 | | simpr 485 |
. . . . . . . 8
β’ (((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
)) β (π β β
β§ π β β
)) |
17 | 12, 13, 7, 8 | paddasslem15 38797 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β β
)) β§ (π β π΄ β§ (π₯ β π β§ π β (π + π)) β§ π β€ (π₯ β¨ π))) β π β ((π + π) + π)) |
18 | 16, 17 | syl3anl3 1414 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β§ (π β π΄ β§ (π₯ β π β§ π β (π + π)) β§ π β€ (π₯ β¨ π))) β π β ((π + π) + π)) |
19 | 18 | 3exp2 1354 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β (π β π΄ β ((π₯ β π β§ π β (π + π)) β (π β€ (π₯ β¨ π) β π β ((π + π) + π))))) |
20 | 19 | imp 407 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β§ π β π΄) β ((π₯ β π β§ π β (π + π)) β (π β€ (π₯ β¨ π) β π β ((π + π) + π)))) |
21 | 20 | rexlimdvv 3210 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β§ π β π΄) β (βπ₯ β π βπ β (π + π)π β€ (π₯ β¨ π) β π β ((π + π) + π))) |
22 | 21 | expimpd 454 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β ((π β π΄ β§ βπ₯ β π βπ β (π + π)π β€ (π₯ β¨ π)) β π β ((π + π) + π))) |
23 | 15, 22 | sylbid 239 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β (π β (π + (π + π)) β π β ((π + π) + π))) |
24 | 23 | ssrdv 3988 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((π β β
β§ (π + π) β β
) β§ (π β β
β§ π β β
))) β (π + (π + π)) β ((π + π) + π)) |