Step | Hyp | Ref
| Expression |
1 | | snssi 4747 |
. . 3
β’ (π β π΄ β {π} β π΄) |
2 | | polat.o |
. . . 4
β’ β₯ =
(ocβπΎ) |
3 | | polat.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
4 | | polat.m |
. . . 4
β’ π = (pmapβπΎ) |
5 | | polat.p |
. . . 4
β’ π =
(β₯πβπΎ) |
6 | 2, 3, 4, 5 | polvalN 37961 |
. . 3
β’ ((πΎ β OL β§ {π} β π΄) β (πβ{π}) = (π΄ β© β©
π β {π} (πβ( β₯ βπ)))) |
7 | 1, 6 | sylan2 594 |
. 2
β’ ((πΎ β OL β§ π β π΄) β (πβ{π}) = (π΄ β© β©
π β {π} (πβ( β₯ βπ)))) |
8 | | 2fveq3 6809 |
. . . . 5
β’ (π = π β (πβ( β₯ βπ)) = (πβ( β₯ βπ))) |
9 | 8 | iinxsng 5024 |
. . . 4
β’ (π β π΄ β β©
π β {π} (πβ( β₯ βπ)) = (πβ( β₯ βπ))) |
10 | 9 | adantl 483 |
. . 3
β’ ((πΎ β OL β§ π β π΄) β β©
π β {π} (πβ( β₯ βπ)) = (πβ( β₯ βπ))) |
11 | 10 | ineq2d 4152 |
. 2
β’ ((πΎ β OL β§ π β π΄) β (π΄ β© β©
π β {π} (πβ( β₯ βπ))) = (π΄ β© (πβ( β₯ βπ)))) |
12 | | olop 37270 |
. . . . 5
β’ (πΎ β OL β πΎ β OP) |
13 | | eqid 2736 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
14 | 13, 3 | atbase 37345 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
15 | 13, 2 | opoccl 37250 |
. . . . 5
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ( β₯ βπ) β (BaseβπΎ)) |
16 | 12, 14, 15 | syl2an 597 |
. . . 4
β’ ((πΎ β OL β§ π β π΄) β ( β₯ βπ) β (BaseβπΎ)) |
17 | 13, 3, 4 | pmapssat 37815 |
. . . 4
β’ ((πΎ β OL β§ ( β₯
βπ) β
(BaseβπΎ)) β
(πβ( β₯
βπ)) β π΄) |
18 | 16, 17 | syldan 592 |
. . 3
β’ ((πΎ β OL β§ π β π΄) β (πβ( β₯ βπ)) β π΄) |
19 | | sseqin2 4155 |
. . 3
β’ ((πβ( β₯ βπ)) β π΄ β (π΄ β© (πβ( β₯ βπ))) = (πβ( β₯ βπ))) |
20 | 18, 19 | sylib 217 |
. 2
β’ ((πΎ β OL β§ π β π΄) β (π΄ β© (πβ( β₯ βπ))) = (πβ( β₯ βπ))) |
21 | 7, 11, 20 | 3eqtrd 2780 |
1
β’ ((πΎ β OL β§ π β π΄) β (πβ{π}) = (πβ( β₯ βπ))) |