Step | Hyp | Ref
| Expression |
1 | | pmapocj.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | pmapocj.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
3 | | pmapocj.f |
. . . 4
β’ πΉ = (pmapβπΎ) |
4 | | pmapocj.p |
. . . 4
β’ + =
(+πβπΎ) |
5 | | pmapocj.r |
. . . 4
β’ π =
(β₯πβπΎ) |
6 | 1, 2, 3, 4, 5 | pmapj2N 39313 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβ(π β¨ π)) = (πβ(πβ((πΉβπ) + (πΉβπ))))) |
7 | 6 | fveq2d 6889 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(πΉβ(π β¨ π))) = (πβ(πβ(πβ((πΉβπ) + (πΉβπ)))))) |
8 | | simp1 1133 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β HL) |
9 | | hllat 38746 |
. . . 4
β’ (πΎ β HL β πΎ β Lat) |
10 | 1, 2 | latjcl 18404 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
11 | 9, 10 | syl3an1 1160 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
12 | | pmapocj.o |
. . . 4
β’ β₯ =
(ocβπΎ) |
13 | 1, 12, 3, 5 | polpmapN 39296 |
. . 3
β’ ((πΎ β HL β§ (π β¨ π) β π΅) β (πβ(πΉβ(π β¨ π))) = (πΉβ( β₯ β(π β¨ π)))) |
14 | 8, 11, 13 | syl2anc 583 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(πΉβ(π β¨ π))) = (πΉβ( β₯ β(π β¨ π)))) |
15 | | eqid 2726 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
16 | 1, 15, 3 | pmapssat 39143 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
17 | 16 | 3adant3 1129 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
18 | 1, 15, 3 | pmapssat 39143 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
19 | 18 | 3adant2 1128 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
20 | 15, 4 | paddssat 39198 |
. . . 4
β’ ((πΎ β HL β§ (πΉβπ) β (AtomsβπΎ) β§ (πΉβπ) β (AtomsβπΎ)) β ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) |
21 | 8, 17, 19, 20 | syl3anc 1368 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) |
22 | 15, 5 | 3polN 39300 |
. . 3
β’ ((πΎ β HL β§ ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) β (πβ(πβ(πβ((πΉβπ) + (πΉβπ))))) = (πβ((πΉβπ) + (πΉβπ)))) |
23 | 8, 21, 22 | syl2anc 583 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(πβ(πβ((πΉβπ) + (πΉβπ))))) = (πβ((πΉβπ) + (πΉβπ)))) |
24 | 7, 14, 23 | 3eqtr3d 2774 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβ( β₯ β(π β¨ π))) = (πβ((πΉβπ) + (πΉβπ)))) |