Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . 4
β’ ((πΌ evalSub π)βπ
) = ((πΌ evalSub π)βπ
) |
2 | | eqid 2726 |
. . . 4
β’ (πΌ mPoly (π βΎs π
)) = (πΌ mPoly (π βΎs π
)) |
3 | | eqid 2726 |
. . . 4
β’ (π βΎs π
) = (π βΎs π
) |
4 | | mpfconst.b |
. . . 4
β’ π΅ = (Baseβπ) |
5 | | eqid 2726 |
. . . 4
β’
(algScβ(πΌ
mPoly (π
βΎs π
))) =
(algScβ(πΌ mPoly
(π βΎs
π
))) |
6 | | mpfconst.i |
. . . 4
β’ (π β πΌ β π) |
7 | | mpfconst.s |
. . . 4
β’ (π β π β CRing) |
8 | | mpfconst.r |
. . . 4
β’ (π β π
β (SubRingβπ)) |
9 | | mpfconst.x |
. . . 4
β’ (π β π β π
) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | evlssca 21994 |
. . 3
β’ (π β (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) = ((π΅ βm πΌ) Γ {π})) |
11 | | eqid 2726 |
. . . . . . 7
β’ (π βs
(π΅ βm πΌ)) = (π βs (π΅ βm πΌ)) |
12 | 1, 2, 3, 11, 4 | evlsrhm 21993 |
. . . . . 6
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β ((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ)))) |
13 | 6, 7, 8, 12 | syl3anc 1368 |
. . . . 5
β’ (π β ((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ)))) |
14 | | eqid 2726 |
. . . . . 6
β’
(Baseβ(πΌ mPoly
(π βΎs
π
))) = (Baseβ(πΌ mPoly (π βΎs π
))) |
15 | | eqid 2726 |
. . . . . 6
β’
(Baseβ(π
βs (π΅ βm πΌ))) = (Baseβ(π βs (π΅ βm πΌ))) |
16 | 14, 15 | rhmf 20387 |
. . . . 5
β’ (((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ))) β ((πΌ evalSub π)βπ
):(Baseβ(πΌ mPoly (π βΎs π
)))βΆ(Baseβ(π βs (π΅ βm πΌ)))) |
17 | | ffn 6711 |
. . . . 5
β’ (((πΌ evalSub π)βπ
):(Baseβ(πΌ mPoly (π βΎs π
)))βΆ(Baseβ(π βs (π΅ βm πΌ))) β ((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
)))) |
18 | 13, 16, 17 | 3syl 18 |
. . . 4
β’ (π β ((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
)))) |
19 | 3 | subrgring 20476 |
. . . . . . 7
β’ (π
β (SubRingβπ) β (π βΎs π
) β Ring) |
20 | 8, 19 | syl 17 |
. . . . . 6
β’ (π β (π βΎs π
) β Ring) |
21 | | eqid 2726 |
. . . . . . 7
β’
(Scalarβ(πΌ
mPoly (π
βΎs π
))) =
(Scalarβ(πΌ mPoly
(π βΎs
π
))) |
22 | 2 | mplring 21920 |
. . . . . . 7
β’ ((πΌ β π β§ (π βΎs π
) β Ring) β (πΌ mPoly (π βΎs π
)) β Ring) |
23 | 2 | mpllmod 21919 |
. . . . . . 7
β’ ((πΌ β π β§ (π βΎs π
) β Ring) β (πΌ mPoly (π βΎs π
)) β LMod) |
24 | | eqid 2726 |
. . . . . . 7
β’
(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
)))) = (Baseβ(Scalarβ(πΌ mPoly (π βΎs π
)))) |
25 | 5, 21, 22, 23, 24, 14 | asclf 21776 |
. . . . . 6
β’ ((πΌ β π β§ (π βΎs π
) β Ring) β (algScβ(πΌ mPoly (π βΎs π
))):(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))βΆ(Baseβ(πΌ mPoly (π βΎs π
)))) |
26 | 6, 20, 25 | syl2anc 583 |
. . . . 5
β’ (π β (algScβ(πΌ mPoly (π βΎs π
))):(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))βΆ(Baseβ(πΌ mPoly (π βΎs π
)))) |
27 | 4 | subrgss 20474 |
. . . . . . . 8
β’ (π
β (SubRingβπ) β π
β π΅) |
28 | 3, 4 | ressbas2 17191 |
. . . . . . . 8
β’ (π
β π΅ β π
= (Baseβ(π βΎs π
))) |
29 | 8, 27, 28 | 3syl 18 |
. . . . . . 7
β’ (π β π
= (Baseβ(π βΎs π
))) |
30 | | ovexd 7440 |
. . . . . . . . 9
β’ (π β (π βΎs π
) β V) |
31 | 2, 6, 30 | mplsca 21914 |
. . . . . . . 8
β’ (π β (π βΎs π
) = (Scalarβ(πΌ mPoly (π βΎs π
)))) |
32 | 31 | fveq2d 6889 |
. . . . . . 7
β’ (π β (Baseβ(π βΎs π
)) =
(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))) |
33 | 29, 32 | eqtrd 2766 |
. . . . . 6
β’ (π β π
= (Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))) |
34 | 9, 33 | eleqtrd 2829 |
. . . . 5
β’ (π β π β (Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))) |
35 | 26, 34 | ffvelcdmd 7081 |
. . . 4
β’ (π β ((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
36 | | fnfvelrn 7076 |
. . . 4
β’ ((((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β§ ((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (Baseβ(πΌ mPoly (π βΎs π
)))) β (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) β ran ((πΌ evalSub π)βπ
)) |
37 | 18, 35, 36 | syl2anc 583 |
. . 3
β’ (π β (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) β ran ((πΌ evalSub π)βπ
)) |
38 | 10, 37 | eqeltrrd 2828 |
. 2
β’ (π β ((π΅ βm πΌ) Γ {π}) β ran ((πΌ evalSub π)βπ
)) |
39 | | mpfconst.q |
. 2
β’ π = ran ((πΌ evalSub π)βπ
) |
40 | 38, 39 | eleqtrrdi 2838 |
1
β’ (π β ((π΅ βm πΌ) Γ {π}) β π) |