Step | Hyp | Ref
| Expression |
1 | | selvffval.i |
. . 3
β’ (π β πΌ β π) |
2 | | selvffval.r |
. . 3
β’ (π β π
β π) |
3 | 1, 2 | selvffval 21678 |
. 2
β’ (π β (πΌ selectVars π
) = (π β π« πΌ β¦ (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π) mPoly π
) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯)))))))) |
4 | | difeq2 4116 |
. . . . . 6
β’ (π = π½ β (πΌ β π) = (πΌ β π½)) |
5 | 4 | oveq1d 7423 |
. . . . 5
β’ (π = π½ β ((πΌ β π) mPoly π
) = ((πΌ β π½) mPoly π
)) |
6 | | oveq1 7415 |
. . . . . 6
β’ (π = π½ β (π mPoly π’) = (π½ mPoly π’)) |
7 | | eleq2 2822 |
. . . . . . . . . . 11
β’ (π = π½ β (π₯ β π β π₯ β π½)) |
8 | | oveq1 7415 |
. . . . . . . . . . . 12
β’ (π = π½ β (π mVar π’) = (π½ mVar π’)) |
9 | 8 | fveq1d 6893 |
. . . . . . . . . . 11
β’ (π = π½ β ((π mVar π’)βπ₯) = ((π½ mVar π’)βπ₯)) |
10 | 4 | oveq1d 7423 |
. . . . . . . . . . . . 13
β’ (π = π½ β ((πΌ β π) mVar π
) = ((πΌ β π½) mVar π
)) |
11 | 10 | fveq1d 6893 |
. . . . . . . . . . . 12
β’ (π = π½ β (((πΌ β π) mVar π
)βπ₯) = (((πΌ β π½) mVar π
)βπ₯)) |
12 | 11 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (π = π½ β (πβ(((πΌ β π) mVar π
)βπ₯)) = (πβ(((πΌ β π½) mVar π
)βπ₯))) |
13 | 7, 9, 12 | ifbieq12d 4556 |
. . . . . . . . . 10
β’ (π = π½ β if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯))) = if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))) |
14 | 13 | mpteq2dv 5250 |
. . . . . . . . 9
β’ (π = π½ β (π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯)))) = (π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) |
15 | 14 | fveq2d 6895 |
. . . . . . . 8
β’ (π = π½ β ((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯))))) = ((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
16 | 15 | csbeq2dv 3900 |
. . . . . . 7
β’ (π = π½ β β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯))))) = β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
17 | 16 | csbeq2dv 3900 |
. . . . . 6
β’ (π = π½ β β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯))))) = β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
18 | 6, 17 | csbeq12dv 3902 |
. . . . 5
β’ (π = π½ β β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯))))) = β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
19 | 5, 18 | csbeq12dv 3902 |
. . . 4
β’ (π = π½ β β¦((πΌ β π) mPoly π
) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯))))) = β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
20 | 19 | mpteq2dv 5250 |
. . 3
β’ (π = π½ β (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π) mPoly π
) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯)))))) = (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))))) |
21 | 20 | adantl 482 |
. 2
β’ ((π β§ π = π½) β (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π) mPoly π
) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π
)βπ₯)))))) = (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))))) |
22 | | selvfval.j |
. . 3
β’ (π β π½ β πΌ) |
23 | 1, 22 | sselpwd 5326 |
. 2
β’ (π β π½ β π« πΌ) |
24 | | fvex 6904 |
. . 3
β’
(Baseβ(πΌ mPoly
π
)) β
V |
25 | | mptexg 7222 |
. . 3
β’
((Baseβ(πΌ
mPoly π
)) β V β
(π β
(Baseβ(πΌ mPoly π
)) β¦
β¦((πΌ β
π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) β V) |
26 | 24, 25 | mp1i 13 |
. 2
β’ (π β (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) β V) |
27 | 3, 21, 23, 26 | fvmptd 7005 |
1
β’ (π β ((πΌ selectVars π
)βπ½) = (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))))) |