Step | Hyp | Ref
| Expression |
1 | | ssid 3967 |
. . 3
β’ π΄ β π΄ |
2 | | eqid 2737 |
. . . 4
β’
(lubβπΎ) =
(lubβπΎ) |
3 | | eqid 2737 |
. . . 4
β’
(ocβπΎ) =
(ocβπΎ) |
4 | | polssat.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
5 | | eqid 2737 |
. . . 4
β’
(pmapβπΎ) =
(pmapβπΎ) |
6 | | polssat.p |
. . . 4
β’ β₯ =
(β₯πβπΎ) |
7 | 2, 3, 4, 5, 6 | polval2N 38372 |
. . 3
β’ ((πΎ β HL β§ π΄ β π΄) β ( β₯ βπ΄) = ((pmapβπΎ)β((ocβπΎ)β((lubβπΎ)βπ΄)))) |
8 | 1, 7 | mpan2 690 |
. 2
β’ (πΎ β HL β ( β₯
βπ΄) =
((pmapβπΎ)β((ocβπΎ)β((lubβπΎ)βπ΄)))) |
9 | | hlop 37827 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OP) |
10 | | eqid 2737 |
. . . . . . . . . . 11
β’
(BaseβπΎ) =
(BaseβπΎ) |
11 | 10, 4 | atbase 37754 |
. . . . . . . . . 10
β’ (π β π΄ β π β (BaseβπΎ)) |
12 | | eqid 2737 |
. . . . . . . . . . 11
β’
(leβπΎ) =
(leβπΎ) |
13 | | eqid 2737 |
. . . . . . . . . . 11
β’
(1.βπΎ) =
(1.βπΎ) |
14 | 10, 12, 13 | ople1 37656 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β π(leβπΎ)(1.βπΎ)) |
15 | 9, 11, 14 | syl2an 597 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄) β π(leβπΎ)(1.βπΎ)) |
16 | 15 | ralrimiva 3144 |
. . . . . . . 8
β’ (πΎ β HL β βπ β π΄ π(leβπΎ)(1.βπΎ)) |
17 | | rabid2 3437 |
. . . . . . . 8
β’ (π΄ = {π β π΄ β£ π(leβπΎ)(1.βπΎ)} β βπ β π΄ π(leβπΎ)(1.βπΎ)) |
18 | 16, 17 | sylibr 233 |
. . . . . . 7
β’ (πΎ β HL β π΄ = {π β π΄ β£ π(leβπΎ)(1.βπΎ)}) |
19 | 18 | fveq2d 6847 |
. . . . . 6
β’ (πΎ β HL β
((lubβπΎ)βπ΄) = ((lubβπΎ)β{π β π΄ β£ π(leβπΎ)(1.βπΎ)})) |
20 | | hlomcmat 37830 |
. . . . . . 7
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat)) |
21 | 10, 13 | op1cl 37650 |
. . . . . . . 8
β’ (πΎ β OP β
(1.βπΎ) β
(BaseβπΎ)) |
22 | 9, 21 | syl 17 |
. . . . . . 7
β’ (πΎ β HL β
(1.βπΎ) β
(BaseβπΎ)) |
23 | 10, 12, 2, 4 | atlatmstc 37784 |
. . . . . . 7
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§
(1.βπΎ) β
(BaseβπΎ)) β
((lubβπΎ)β{π β π΄ β£ π(leβπΎ)(1.βπΎ)}) = (1.βπΎ)) |
24 | 20, 22, 23 | syl2anc 585 |
. . . . . 6
β’ (πΎ β HL β
((lubβπΎ)β{π β π΄ β£ π(leβπΎ)(1.βπΎ)}) = (1.βπΎ)) |
25 | 19, 24 | eqtr2d 2778 |
. . . . 5
β’ (πΎ β HL β
(1.βπΎ) =
((lubβπΎ)βπ΄)) |
26 | 25 | fveq2d 6847 |
. . . 4
β’ (πΎ β HL β
((ocβπΎ)β(1.βπΎ)) = ((ocβπΎ)β((lubβπΎ)βπ΄))) |
27 | | eqid 2737 |
. . . . . 6
β’
(0.βπΎ) =
(0.βπΎ) |
28 | 27, 13, 3 | opoc1 37667 |
. . . . 5
β’ (πΎ β OP β
((ocβπΎ)β(1.βπΎ)) = (0.βπΎ)) |
29 | 9, 28 | syl 17 |
. . . 4
β’ (πΎ β HL β
((ocβπΎ)β(1.βπΎ)) = (0.βπΎ)) |
30 | 26, 29 | eqtr3d 2779 |
. . 3
β’ (πΎ β HL β
((ocβπΎ)β((lubβπΎ)βπ΄)) = (0.βπΎ)) |
31 | 30 | fveq2d 6847 |
. 2
β’ (πΎ β HL β
((pmapβπΎ)β((ocβπΎ)β((lubβπΎ)βπ΄))) = ((pmapβπΎ)β(0.βπΎ))) |
32 | | hlatl 37825 |
. . 3
β’ (πΎ β HL β πΎ β AtLat) |
33 | 27, 5 | pmap0 38231 |
. . 3
β’ (πΎ β AtLat β
((pmapβπΎ)β(0.βπΎ)) = β
) |
34 | 32, 33 | syl 17 |
. 2
β’ (πΎ β HL β
((pmapβπΎ)β(0.βπΎ)) = β
) |
35 | 8, 31, 34 | 3eqtrd 2781 |
1
β’ (πΎ β HL β ( β₯
βπ΄) =
β
) |