Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
2 | | eqid 2733 |
. . 3
β’
(β₯πβπΎ) = (β₯πβπΎ) |
3 | | pmapsubcl.c |
. . 3
β’ πΆ = (PSubClβπΎ) |
4 | 1, 2, 3 | ispsubclN 38808 |
. 2
β’ (πΎ β HL β (π β πΆ β (π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π))) |
5 | | hlop 38232 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β OP) |
6 | 5 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β πΎ β OP) |
7 | | hlclat 38228 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β CLat) |
8 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β πΎ β CLat) |
9 | 1, 2 | polssatN 38779 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β
((β₯πβπΎ)βπ) β (AtomsβπΎ)) |
10 | | pmapsubcl.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΎ) |
11 | 10, 1 | atssbase 38160 |
. . . . . . . . . 10
β’
(AtomsβπΎ)
β π΅ |
12 | 9, 11 | sstrdi 3995 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β
((β₯πβπΎ)βπ) β π΅) |
13 | | eqid 2733 |
. . . . . . . . . 10
β’
(lubβπΎ) =
(lubβπΎ) |
14 | 10, 13 | clatlubcl 18456 |
. . . . . . . . 9
β’ ((πΎ β CLat β§
((β₯πβπΎ)βπ) β π΅) β ((lubβπΎ)β((β₯πβπΎ)βπ)) β π΅) |
15 | 8, 12, 14 | syl2anc 585 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β ((lubβπΎ)β((β₯πβπΎ)βπ)) β π΅) |
16 | | eqid 2733 |
. . . . . . . . 9
β’
(ocβπΎ) =
(ocβπΎ) |
17 | 10, 16 | opoccl 38064 |
. . . . . . . 8
β’ ((πΎ β OP β§
((lubβπΎ)β((β₯πβπΎ)βπ)) β π΅) β ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β π΅) |
18 | 6, 15, 17 | syl2anc 585 |
. . . . . . 7
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β π΅) |
19 | 18 | ex 414 |
. . . . . 6
β’ (πΎ β HL β (π β (AtomsβπΎ) β ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β π΅)) |
20 | 19 | adantrd 493 |
. . . . 5
β’ (πΎ β HL β ((π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π) β ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β π΅)) |
21 | | pmapsubcl.m |
. . . . . . . . . 10
β’ π = (pmapβπΎ) |
22 | 13, 16, 1, 21, 2 | polval2N 38777 |
. . . . . . . . 9
β’ ((πΎ β HL β§
((β₯πβπΎ)βπ) β (AtomsβπΎ)) β
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))))) |
23 | 9, 22 | syldan 592 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))))) |
24 | 23 | ex 414 |
. . . . . . 7
β’ (πΎ β HL β (π β (AtomsβπΎ) β
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ)))))) |
25 | | eqeq1 2737 |
. . . . . . . 8
β’
(((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π β
(((β₯πβπΎ)β((β₯πβπΎ)βπ)) = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ)))) β π = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ)))))) |
26 | 25 | biimpcd 248 |
. . . . . . 7
β’
(((β₯πβπΎ)β((β₯πβπΎ)βπ)) = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ)))) β
(((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π β π = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ)))))) |
27 | 24, 26 | syl6 35 |
. . . . . 6
β’ (πΎ β HL β (π β (AtomsβπΎ) β
(((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π β π = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))))))) |
28 | 27 | impd 412 |
. . . . 5
β’ (πΎ β HL β ((π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π) β π = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ)))))) |
29 | 20, 28 | jcad 514 |
. . . 4
β’ (πΎ β HL β ((π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π) β (((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β π΅ β§ π = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))))))) |
30 | | fveq2 6892 |
. . . . 5
β’ (π¦ = ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β (πβπ¦) = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))))) |
31 | 30 | rspceeqv 3634 |
. . . 4
β’
((((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))) β π΅ β§ π = (πβ((ocβπΎ)β((lubβπΎ)β((β₯πβπΎ)βπ))))) β βπ¦ β π΅ π = (πβπ¦)) |
32 | 29, 31 | syl6 35 |
. . 3
β’ (πΎ β HL β ((π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π) β βπ¦ β π΅ π = (πβπ¦))) |
33 | 10, 1, 21 | pmapssat 38630 |
. . . . 5
β’ ((πΎ β HL β§ π¦ β π΅) β (πβπ¦) β (AtomsβπΎ)) |
34 | 10, 21, 2 | 2polpmapN 38784 |
. . . . 5
β’ ((πΎ β HL β§ π¦ β π΅) β
((β₯πβπΎ)β((β₯πβπΎ)β(πβπ¦))) = (πβπ¦)) |
35 | | sseq1 4008 |
. . . . . . 7
β’ (π = (πβπ¦) β (π β (AtomsβπΎ) β (πβπ¦) β (AtomsβπΎ))) |
36 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π = (πβπ¦) β
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = ((β₯πβπΎ)β((β₯πβπΎ)β(πβπ¦)))) |
37 | | id 22 |
. . . . . . . 8
β’ (π = (πβπ¦) β π = (πβπ¦)) |
38 | 36, 37 | eqeq12d 2749 |
. . . . . . 7
β’ (π = (πβπ¦) β
(((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π β ((β₯πβπΎ)β((β₯πβπΎ)β(πβπ¦))) = (πβπ¦))) |
39 | 35, 38 | anbi12d 632 |
. . . . . 6
β’ (π = (πβπ¦) β ((π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π) β ((πβπ¦) β (AtomsβπΎ) β§ ((β₯πβπΎ)β((β₯πβπΎ)β(πβπ¦))) = (πβπ¦)))) |
40 | 39 | biimprcd 249 |
. . . . 5
β’ (((πβπ¦) β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)β(πβπ¦))) = (πβπ¦)) β (π = (πβπ¦) β (π β (AtomsβπΎ) β§ ((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π))) |
41 | 33, 34, 40 | syl2anc 585 |
. . . 4
β’ ((πΎ β HL β§ π¦ β π΅) β (π = (πβπ¦) β (π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π))) |
42 | 41 | rexlimdva 3156 |
. . 3
β’ (πΎ β HL β (βπ¦ β π΅ π = (πβπ¦) β (π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π))) |
43 | 32, 42 | impbid 211 |
. 2
β’ (πΎ β HL β ((π β (AtomsβπΎ) β§
((β₯πβπΎ)β((β₯πβπΎ)βπ)) = π) β βπ¦ β π΅ π = (πβπ¦))) |
44 | 4, 43 | bitrd 279 |
1
β’ (πΎ β HL β (π β πΆ β βπ¦ β π΅ π = (πβπ¦))) |