Step | Hyp | Ref
| Expression |
1 | | docaval.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
2 | | docaval.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
3 | | docaval.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
4 | | docaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | docaval.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
6 | | docaval.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
7 | | docaval.n |
. . . . 5
β’ π = ((ocAβπΎ)βπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | docafvalN 39588 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))) |
9 | 8 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β π = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))) |
10 | 9 | fveq1d 6845 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβπ) = ((π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))βπ)) |
11 | 5 | fvexi 6857 |
. . . . . 6
β’ π β V |
12 | 11 | elpw2 5303 |
. . . . 5
β’ (π β π« π β π β π) |
13 | 12 | biimpri 227 |
. . . 4
β’ (π β π β π β π« π) |
14 | 13 | adantl 483 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β π« π) |
15 | | fvex 6856 |
. . 3
β’ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π)) β V |
16 | | sseq1 3970 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ β π§ β π β π§)) |
17 | 16 | rabbidv 3416 |
. . . . . . . . 9
β’ (π₯ = π β {π§ β ran πΌ β£ π₯ β π§} = {π§ β ran πΌ β£ π β π§}) |
18 | 17 | inteqd 4913 |
. . . . . . . 8
β’ (π₯ = π β β© {π§ β ran πΌ β£ π₯ β π§} = β© {π§ β ran πΌ β£ π β π§}) |
19 | 18 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π β (β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§}) = (β‘πΌββ© {π§ β ran πΌ β£ π β π§})) |
20 | 19 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β ( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) = ( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))) |
21 | 20 | oveq1d 7373 |
. . . . 5
β’ (π₯ = π β (( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) = (( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ))) |
22 | 21 | fvoveq1d 7380 |
. . . 4
β’ (π₯ = π β (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π))) |
23 | | eqid 2737 |
. . . 4
β’ (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π))) = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π))) |
24 | 22, 23 | fvmptg 6947 |
. . 3
β’ ((π β π« π β§ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π)) β V) β ((π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))βπ) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π))) |
25 | 14, 15, 24 | sylancl 587 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))βπ) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π))) |
26 | 10, 25 | eqtrd 2777 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβπ) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π))) |