Step | Hyp | Ref
| Expression |
1 | | ssel 3974 |
. . . . . . 7
β’ (π β π β (π β π β π β π)) |
2 | 1 | orim2d 963 |
. . . . . 6
β’ (π β π β ((π β π β¨ π β π) β (π β π β¨ π β π))) |
3 | | ssrexv 4050 |
. . . . . . . 8
β’ (π β π β (βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β π π(leβπΎ)(π(joinβπΎ)π))) |
4 | 3 | reximdv 3168 |
. . . . . . 7
β’ (π β π β (βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) |
5 | 4 | anim2d 610 |
. . . . . 6
β’ (π β π β ((π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)))) |
6 | 2, 5 | orim12d 961 |
. . . . 5
β’ (π β π β (((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
7 | 6 | adantl 480 |
. . . 4
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β (((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
8 | | simpl1 1189 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β π΅) |
9 | | simpl3 1191 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
10 | | sstr 3989 |
. . . . . . 7
β’ ((π β π β§ π β π΄) β π β π΄) |
11 | 10 | 3ad2antr2 1187 |
. . . . . 6
β’ ((π β π β§ (πΎ β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
12 | 11 | ancoms 457 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
13 | | eqid 2730 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
14 | | eqid 2730 |
. . . . . 6
β’
(joinβπΎ) =
(joinβπΎ) |
15 | | padd0.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
16 | | padd0.p |
. . . . . 6
β’ + =
(+πβπΎ) |
17 | 13, 14, 15, 16 | elpadd 38973 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
18 | 8, 9, 12, 17 | syl3anc 1369 |
. . . 4
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
19 | | simpl2 1190 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
20 | 13, 14, 15, 16 | elpadd 38973 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
21 | 8, 9, 19, 20 | syl3anc 1369 |
. . . 4
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
22 | 7, 18, 21 | 3imtr4d 293 |
. . 3
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β (π + π) β π β (π + π))) |
23 | 22 | ssrdv 3987 |
. 2
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β (π + π) β (π + π)) |
24 | 23 | ex 411 |
1
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β π β (π + π) β (π + π))) |