Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β πΎ β HL) |
2 | | pmapjat.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | pmapjat.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
4 | | pmapjat.m |
. . . . 5
β’ π = (pmapβπΎ) |
5 | 2, 3, 4 | pmapssat 38225 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (πβπ) β π΄) |
6 | 5 | 3ad2antr1 1189 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβπ) β π΄) |
7 | | simpr2 1196 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β π β π΄) |
8 | 2, 3 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β π΅) |
9 | 7, 8 | syl 17 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β π β π΅) |
10 | 2, 3, 4 | pmapssat 38225 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (πβπ) β π΄) |
11 | 9, 10 | syldan 592 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβπ) β π΄) |
12 | | simpr3 1197 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β π
β π΄) |
13 | 2, 3 | atbase 37754 |
. . . . 5
β’ (π
β π΄ β π
β π΅) |
14 | 12, 13 | syl 17 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β π
β π΅) |
15 | 2, 3, 4 | pmapssat 38225 |
. . . 4
β’ ((πΎ β HL β§ π
β π΅) β (πβπ
) β π΄) |
16 | 14, 15 | syldan 592 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβπ
) β π΄) |
17 | | pmapjat.p |
. . . 4
β’ + =
(+πβπΎ) |
18 | 3, 17 | paddass 38304 |
. . 3
β’ ((πΎ β HL β§ ((πβπ) β π΄ β§ (πβπ) β π΄ β§ (πβπ
) β π΄)) β (((πβπ) + (πβπ)) + (πβπ
)) = ((πβπ) + ((πβπ) + (πβπ
)))) |
19 | 1, 6, 11, 16, 18 | syl13anc 1373 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (((πβπ) + (πβπ)) + (πβπ
)) = ((πβπ) + ((πβπ) + (πβπ
)))) |
20 | | hllat 37828 |
. . . . . 6
β’ (πΎ β HL β πΎ β Lat) |
21 | 20 | adantr 482 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β πΎ β Lat) |
22 | | simpr1 1195 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β π β π΅) |
23 | | pmapjat.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
24 | 2, 23 | latjcl 18329 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
25 | 21, 22, 9, 24 | syl3anc 1372 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (π β¨ π) β π΅) |
26 | 2, 23, 3, 4, 17 | pmapjat1 38319 |
. . . 4
β’ ((πΎ β HL β§ (π β¨ π) β π΅ β§ π
β π΄) β (πβ((π β¨ π) β¨ π
)) = ((πβ(π β¨ π)) + (πβπ
))) |
27 | 1, 25, 12, 26 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβ((π β¨ π) β¨ π
)) = ((πβ(π β¨ π)) + (πβπ
))) |
28 | 2, 23 | latjass 18373 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π
β π΅)) β ((π β¨ π) β¨ π
) = (π β¨ (π β¨ π
))) |
29 | 21, 22, 9, 14, 28 | syl13anc 1373 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β ((π β¨ π) β¨ π
) = (π β¨ (π β¨ π
))) |
30 | 29 | fveq2d 6847 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβ((π β¨ π) β¨ π
)) = (πβ(π β¨ (π β¨ π
)))) |
31 | 2, 23, 3, 4, 17 | pmapjat1 38319 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (πβ(π β¨ π)) = ((πβπ) + (πβπ))) |
32 | 31 | 3adant3r3 1185 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβ(π β¨ π)) = ((πβπ) + (πβπ))) |
33 | 32 | oveq1d 7373 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β ((πβ(π β¨ π)) + (πβπ
)) = (((πβπ) + (πβπ)) + (πβπ
))) |
34 | 27, 30, 33 | 3eqtr3d 2785 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβ(π β¨ (π β¨ π
))) = (((πβπ) + (πβπ)) + (πβπ
))) |
35 | 2, 23, 3, 4, 17 | pmapjat1 38319 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π
β π΄) β (πβ(π β¨ π
)) = ((πβπ) + (πβπ
))) |
36 | 1, 9, 12, 35 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβ(π β¨ π
)) = ((πβπ) + (πβπ
))) |
37 | 36 | oveq2d 7374 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β ((πβπ) + (πβ(π β¨ π
))) = ((πβπ) + ((πβπ) + (πβπ
)))) |
38 | 19, 34, 37 | 3eqtr4d 2787 |
1
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π
β π΄)) β (πβ(π β¨ (π β¨ π
))) = ((πβπ) + (πβ(π β¨ π
)))) |