Step | Hyp | Ref
| Expression |
1 | | dochval.n |
. . 3
β’ π = ((ocHβπΎ)βπ) |
2 | | dochval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | dochval.g |
. . . . 5
β’ πΊ = (glbβπΎ) |
4 | | dochval.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
5 | | dochval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | 2, 3, 4, 5 | dochffval 39841 |
. . . 4
β’ (πΎ β π β (ocHβπΎ) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))) |
7 | 6 | fveq1d 6849 |
. . 3
β’ (πΎ β π β ((ocHβπΎ)βπ) = ((π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))βπ)) |
8 | 1, 7 | eqtrid 2789 |
. 2
β’ (πΎ β π β π = ((π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))βπ)) |
9 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π β ((DVecHβπΎ)βπ€) = ((DVecHβπΎ)βπ)) |
10 | | dochval.u |
. . . . . . . 8
β’ π = ((DVecHβπΎ)βπ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β ((DVecHβπΎ)βπ€) = π) |
12 | 11 | fveq2d 6851 |
. . . . . 6
β’ (π€ = π β (Baseβ((DVecHβπΎ)βπ€)) = (Baseβπ)) |
13 | | dochval.v |
. . . . . 6
β’ π = (Baseβπ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β (Baseβ((DVecHβπΎ)βπ€)) = π) |
15 | 14 | pweqd 4582 |
. . . 4
β’ (π€ = π β π«
(Baseβ((DVecHβπΎ)βπ€)) = π« π) |
16 | | fveq2 6847 |
. . . . . 6
β’ (π€ = π β ((DIsoHβπΎ)βπ€) = ((DIsoHβπΎ)βπ)) |
17 | | dochval.i |
. . . . . 6
β’ πΌ = ((DIsoHβπΎ)βπ) |
18 | 16, 17 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β ((DIsoHβπΎ)βπ€) = πΌ) |
19 | 18 | fveq1d 6849 |
. . . . . . . . 9
β’ (π€ = π β (((DIsoHβπΎ)βπ€)βπ¦) = (πΌβπ¦)) |
20 | 19 | sseq2d 3981 |
. . . . . . . 8
β’ (π€ = π β (π₯ β (((DIsoHβπΎ)βπ€)βπ¦) β π₯ β (πΌβπ¦))) |
21 | 20 | rabbidv 3418 |
. . . . . . 7
β’ (π€ = π β {π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)} = {π¦ β π΅ β£ π₯ β (πΌβπ¦)}) |
22 | 21 | fveq2d 6851 |
. . . . . 6
β’ (π€ = π β (πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}) = (πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)})) |
23 | 22 | fveq2d 6851 |
. . . . 5
β’ (π€ = π β ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})) = ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))) |
24 | 18, 23 | fveq12d 6854 |
. . . 4
β’ (π€ = π β (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}))) = (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)})))) |
25 | 15, 24 | mpteq12dv 5201 |
. . 3
β’ (π€ = π β (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))) = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))) |
26 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}))))) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}))))) |
27 | 13 | fvexi 6861 |
. . . . 5
β’ π β V |
28 | 27 | pwex 5340 |
. . . 4
β’ π«
π β V |
29 | 28 | mptex 7178 |
. . 3
β’ (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)})))) β V |
30 | 25, 26, 29 | fvmpt 6953 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))βπ) = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))) |
31 | 8, 30 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β π = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))) |