Step | Hyp | Ref
| Expression |
1 | | dochval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | dochval.g |
. . . . 5
β’ πΊ = (glbβπΎ) |
3 | | dochval.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
4 | | dochval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | dochval.i |
. . . . 5
β’ πΌ = ((DIsoHβπΎ)βπ) |
6 | | dochval.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
7 | | dochval.v |
. . . . 5
β’ π = (Baseβπ) |
8 | | dochval.n |
. . . . 5
β’ π = ((ocHβπΎ)βπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | dochfval 39842 |
. . . 4
β’ ((πΎ β π β§ π β π») β π = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))) |
10 | 9 | adantr 482 |
. . 3
β’ (((πΎ β π β§ π β π») β§ π β π) β π = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))) |
11 | 10 | fveq1d 6849 |
. 2
β’ (((πΎ β π β§ π β π») β§ π β π) β (πβπ) = ((π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))βπ)) |
12 | 7 | fvexi 6861 |
. . . . . 6
β’ π β V |
13 | 12 | elpw2 5307 |
. . . . 5
β’ (π β π« π β π β π) |
14 | 13 | biimpri 227 |
. . . 4
β’ (π β π β π β π« π) |
15 | 14 | adantl 483 |
. . 3
β’ (((πΎ β π β§ π β π») β§ π β π) β π β π« π) |
16 | | fvex 6860 |
. . 3
β’ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)}))) β V |
17 | | sseq1 3974 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β (πΌβπ¦) β π β (πΌβπ¦))) |
18 | 17 | rabbidv 3418 |
. . . . . . 7
β’ (π₯ = π β {π¦ β π΅ β£ π₯ β (πΌβπ¦)} = {π¦ β π΅ β£ π β (πΌβπ¦)}) |
19 | 18 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = π β (πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}) = (πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)})) |
20 | 19 | fveq2d 6851 |
. . . . 5
β’ (π₯ = π β ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)})) = ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)}))) |
21 | 20 | fveq2d 6851 |
. . . 4
β’ (π₯ = π β (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))) = (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)})))) |
22 | | eqid 2737 |
. . . 4
β’ (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)})))) = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)})))) |
23 | 21, 22 | fvmptg 6951 |
. . 3
β’ ((π β π« π β§ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)}))) β V) β ((π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))βπ) = (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)})))) |
24 | 15, 16, 23 | sylancl 587 |
. 2
β’ (((πΎ β π β§ π β π») β§ π β π) β ((π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))βπ) = (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)})))) |
25 | 11, 24 | eqtrd 2777 |
1
β’ (((πΎ β π β§ π β π») β§ π β π) β (πβπ) = (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)})))) |