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 38795 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβ(π β¨ π)) = (πβ(πβ((πΉβπ) + (πΉβπ))))) |
7 | 6 | fveq2d 6895 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(πΉβ(π β¨ π))) = (πβ(πβ(πβ((πΉβπ) + (πΉβπ)))))) |
8 | | simp1 1136 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β HL) |
9 | | hllat 38228 |
. . . 4
β’ (πΎ β HL β πΎ β Lat) |
10 | 1, 2 | latjcl 18391 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
11 | 9, 10 | syl3an1 1163 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
12 | | pmapocj.o |
. . . 4
β’ β₯ =
(ocβπΎ) |
13 | 1, 12, 3, 5 | polpmapN 38778 |
. . 3
β’ ((πΎ β HL β§ (π β¨ π) β π΅) β (πβ(πΉβ(π β¨ π))) = (πΉβ( β₯ β(π β¨ π)))) |
14 | 8, 11, 13 | syl2anc 584 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(πΉβ(π β¨ π))) = (πΉβ( β₯ β(π β¨ π)))) |
15 | | eqid 2732 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
16 | 1, 15, 3 | pmapssat 38625 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
17 | 16 | 3adant3 1132 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
18 | 1, 15, 3 | pmapssat 38625 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
19 | 18 | 3adant2 1131 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
20 | 15, 4 | paddssat 38680 |
. . . 4
β’ ((πΎ β HL β§ (πΉβπ) β (AtomsβπΎ) β§ (πΉβπ) β (AtomsβπΎ)) β ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) |
21 | 8, 17, 19, 20 | syl3anc 1371 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) |
22 | 15, 5 | 3polN 38782 |
. . 3
β’ ((πΎ β HL β§ ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) β (πβ(πβ(πβ((πΉβπ) + (πΉβπ))))) = (πβ((πΉβπ) + (πΉβπ)))) |
23 | 8, 21, 22 | syl2anc 584 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(πβ(πβ((πΉβπ) + (πΉβπ))))) = (πβ((πΉβπ) + (πΉβπ)))) |
24 | 7, 14, 23 | 3eqtr3d 2780 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβ( β₯ β(π β¨ π))) = (πβ((πΉβπ) + (πΉβπ)))) |