Step | Hyp | Ref
| Expression |
1 | | selvval.i |
. . . 4
β’ (π β πΌ β π) |
2 | | selvval.r |
. . . 4
β’ (π β π
β π) |
3 | | selvval.j |
. . . 4
β’ (π β π½ β πΌ) |
4 | 1, 2, 3 | selvfval 21550 |
. . 3
β’ (π β ((πΌ selectVars π
)βπ½) = (π β (Baseβ(πΌ mPoly π
)) β¦ β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))))) |
5 | | coeq2 5818 |
. . . . . . . . . 10
β’ (π = πΉ β (π β π) = (π β πΉ)) |
6 | 5 | fveq2d 6850 |
. . . . . . . . 9
β’ (π = πΉ β (((πΌ evalSub π‘)βran π)β(π β π)) = (((πΌ evalSub π‘)βran π)β(π β πΉ))) |
7 | 6 | fveq1d 6848 |
. . . . . . . 8
β’ (π = πΉ β ((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
8 | 7 | csbeq2dv 3866 |
. . . . . . 7
β’ (π = πΉ β β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
9 | 8 | csbeq2dv 3866 |
. . . . . 6
β’ (π = πΉ β β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
10 | 9 | csbeq2dv 3866 |
. . . . 5
β’ (π = πΉ β β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
11 | 10 | csbeq2dv 3866 |
. . . 4
β’ (π = πΉ β β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
12 | 11 | adantl 483 |
. . 3
β’ ((π β§ π = πΉ) β β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
13 | | selvval.f |
. . . 4
β’ (π β πΉ β π΅) |
14 | | selvval.b |
. . . . 5
β’ π΅ = (Baseβπ) |
15 | | selvval.p |
. . . . . 6
β’ π = (πΌ mPoly π
) |
16 | 15 | fveq2i 6849 |
. . . . 5
β’
(Baseβπ) =
(Baseβ(πΌ mPoly π
)) |
17 | 14, 16 | eqtri 2761 |
. . . 4
β’ π΅ = (Baseβ(πΌ mPoly π
)) |
18 | 13, 17 | eleqtrdi 2844 |
. . 3
β’ (π β πΉ β (Baseβ(πΌ mPoly π
))) |
19 | | fvex 6859 |
. . . . . . . 8
β’ ((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) β V |
20 | 19 | csbex 5272 |
. . . . . . 7
β’
β¦(π
β (algScβπ’)) /
πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) β V |
21 | 20 | csbex 5272 |
. . . . . 6
β’
β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) β V |
22 | 21 | csbex 5272 |
. . . . 5
β’
β¦(π½
mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) β V |
23 | 22 | csbex 5272 |
. . . 4
β’
β¦((πΌ
β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) β V |
24 | 23 | a1i 11 |
. . 3
β’ (π β β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) β V) |
25 | 4, 12, 18, 24 | fvmptd 6959 |
. 2
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) = β¦((πΌ β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
26 | | ovex 7394 |
. . 3
β’ ((πΌ β π½) mPoly π
) β V |
27 | | selvval.u |
. . . . 5
β’ π = ((πΌ β π½) mPoly π
) |
28 | 27 | eqeq2i 2746 |
. . . 4
β’ (π’ = π β π’ = ((πΌ β π½) mPoly π
)) |
29 | | oveq2 7369 |
. . . . . 6
β’ (π’ = π β (π½ mPoly π’) = (π½ mPoly π)) |
30 | | fveq2 6846 |
. . . . . . . . 9
β’ (π’ = π β (algScβπ’) = (algScβπ)) |
31 | 30 | coeq2d 5822 |
. . . . . . . 8
β’ (π’ = π β (π β (algScβπ’)) = (π β (algScβπ))) |
32 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π’ = π β (π½ mVar π’) = (π½ mVar π)) |
33 | 32 | fveq1d 6848 |
. . . . . . . . . . 11
β’ (π’ = π β ((π½ mVar π’)βπ₯) = ((π½ mVar π)βπ₯)) |
34 | 33 | ifeq1d 4509 |
. . . . . . . . . 10
β’ (π’ = π β if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))) = if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))) |
35 | 34 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π’ = π β (π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))) = (π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) |
36 | 35 | fveq2d 6850 |
. . . . . . . 8
β’ (π’ = π β ((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
37 | 31, 36 | csbeq12dv 3868 |
. . . . . . 7
β’ (π’ = π β β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
38 | 37 | csbeq2dv 3866 |
. . . . . 6
β’ (π’ = π β β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
39 | 29, 38 | csbeq12dv 3868 |
. . . . 5
β’ (π’ = π β β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(π½ mPoly π) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
40 | | ovex 7394 |
. . . . . 6
β’ (π½ mPoly π) β V |
41 | | selvval.t |
. . . . . . . 8
β’ π = (π½ mPoly π) |
42 | 41 | eqeq2i 2746 |
. . . . . . 7
β’ (π‘ = π β π‘ = (π½ mPoly π)) |
43 | | fveq2 6846 |
. . . . . . . . 9
β’ (π‘ = π β (algScβπ‘) = (algScβπ)) |
44 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (πΌ evalSub π‘) = (πΌ evalSub π)) |
45 | 44 | fveq1d 6848 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((πΌ evalSub π‘)βran π) = ((πΌ evalSub π)βran π)) |
46 | 45 | fveq1d 6848 |
. . . . . . . . . . 11
β’ (π‘ = π β (((πΌ evalSub π‘)βran π)β(π β πΉ)) = (((πΌ evalSub π)βran π)β(π β πΉ))) |
47 | 46 | fveq1d 6848 |
. . . . . . . . . 10
β’ (π‘ = π β ((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
48 | 47 | csbeq2dv 3866 |
. . . . . . . . 9
β’ (π‘ = π β β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
49 | 43, 48 | csbeq12dv 3868 |
. . . . . . . 8
β’ (π‘ = π β β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(algScβπ) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))))) |
50 | | fvex 6859 |
. . . . . . . . 9
β’
(algScβπ)
β V |
51 | | selvval.c |
. . . . . . . . . . 11
β’ πΆ = (algScβπ) |
52 | 51 | eqeq2i 2746 |
. . . . . . . . . 10
β’ (π = πΆ β π = (algScβπ)) |
53 | | coeq1 5817 |
. . . . . . . . . . . 12
β’ (π = πΆ β (π β (algScβπ)) = (πΆ β (algScβπ))) |
54 | | fveq1 6845 |
. . . . . . . . . . . . . . 15
β’ (π = πΆ β (πβ(((πΌ β π½) mVar π
)βπ₯)) = (πΆβ(((πΌ β π½) mVar π
)βπ₯))) |
55 | 54 | ifeq2d 4510 |
. . . . . . . . . . . . . 14
β’ (π = πΆ β if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))) = if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))) |
56 | 55 | mpteq2dv 5211 |
. . . . . . . . . . . . 13
β’ (π = πΆ β (π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯)))) = (π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) |
57 | 56 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π = πΆ β ((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
58 | 53, 57 | csbeq12dv 3868 |
. . . . . . . . . . 11
β’ (π = πΆ β β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = β¦(πΆ β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
59 | 51 | fvexi 6860 |
. . . . . . . . . . . . 13
β’ πΆ β V |
60 | | fvex 6859 |
. . . . . . . . . . . . 13
β’
(algScβπ)
β V |
61 | 59, 60 | coex 7871 |
. . . . . . . . . . . 12
β’ (πΆ β (algScβπ)) β V |
62 | | selvval.d |
. . . . . . . . . . . . . 14
β’ π· = (πΆ β (algScβπ)) |
63 | 62 | eqeq2i 2746 |
. . . . . . . . . . . . 13
β’ (π = π· β π = (πΆ β (algScβπ))) |
64 | | rneq 5895 |
. . . . . . . . . . . . . . . 16
β’ (π = π· β ran π = ran π·) |
65 | 64 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ (π = π· β ((πΌ evalSub π)βran π) = ((πΌ evalSub π)βran π·)) |
66 | | coeq1 5817 |
. . . . . . . . . . . . . . 15
β’ (π = π· β (π β πΉ) = (π· β πΉ)) |
67 | 65, 66 | fveq12d 6853 |
. . . . . . . . . . . . . 14
β’ (π = π· β (((πΌ evalSub π)βran π)β(π β πΉ)) = (((πΌ evalSub π)βran π·)β(π· β πΉ))) |
68 | 67 | fveq1d 6848 |
. . . . . . . . . . . . 13
β’ (π = π· β ((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
69 | 63, 68 | sylbir 234 |
. . . . . . . . . . . 12
β’ (π = (πΆ β (algScβπ)) β ((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
70 | 61, 69 | csbie 3895 |
. . . . . . . . . . 11
β’
β¦(πΆ
β (algScβπ)) /
πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) |
71 | 58, 70 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π = πΆ β β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
72 | 52, 71 | sylbir 234 |
. . . . . . . . 9
β’ (π = (algScβπ) β β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
73 | 50, 72 | csbie 3895 |
. . . . . . . 8
β’
β¦(algScβπ) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) |
74 | 49, 73 | eqtrdi 2789 |
. . . . . . 7
β’ (π‘ = π β β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
75 | 42, 74 | sylbir 234 |
. . . . . 6
β’ (π‘ = (π½ mPoly π) β β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
76 | 40, 75 | csbie 3895 |
. . . . 5
β’
β¦(π½
mPoly π) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) |
77 | 39, 76 | eqtrdi 2789 |
. . . 4
β’ (π’ = π β β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
78 | 28, 77 | sylbir 234 |
. . 3
β’ (π’ = ((πΌ β π½) mPoly π
) β β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |
79 | 26, 78 | csbie 3895 |
. 2
β’
β¦((πΌ
β π½) mPoly π
) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π
)βπ₯))))) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯))))) |
80 | 25, 79 | eqtrdi 2789 |
1
β’ (π β (((πΌ selectVars π
)βπ½)βπΉ) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π
)βπ₯)))))) |