Step | Hyp | Ref
| Expression |
1 | | 1on 8429 |
. . . . . 6
β’
1o β On |
2 | | evls1sca.s |
. . . . . 6
β’ (π β π β CRing) |
3 | | evls1sca.r |
. . . . . 6
β’ (π β π
β (SubRingβπ)) |
4 | | eqid 2737 |
. . . . . . 7
β’
((1o evalSub π)βπ
) = ((1o evalSub π)βπ
) |
5 | | eqid 2737 |
. . . . . . 7
β’
(1o mPoly π) = (1o mPoly π) |
6 | | evls1sca.u |
. . . . . . 7
β’ π = (π βΎs π
) |
7 | | eqid 2737 |
. . . . . . 7
β’ (π βs
(π΅ βm
1o)) = (π
βs (π΅ βm
1o)) |
8 | | evls1sca.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
9 | 4, 5, 6, 7, 8 | evlsrhm 21514 |
. . . . . 6
β’
((1o β On β§ π β CRing β§ π
β (SubRingβπ)) β ((1o evalSub π)βπ
) β ((1o mPoly π) RingHom (π βs (π΅ βm
1o)))) |
10 | 1, 2, 3, 9 | mp3an2i 1467 |
. . . . 5
β’ (π β ((1o evalSub
π)βπ
) β ((1o mPoly π) RingHom (π βs (π΅ βm
1o)))) |
11 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(1o mPoly π)) = (Baseβ(1o mPoly π)) |
12 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(π
βs (π΅ βm 1o))) =
(Baseβ(π
βs (π΅ βm
1o))) |
13 | 11, 12 | rhmf 20167 |
. . . . 5
β’
(((1o evalSub π)βπ
) β ((1o mPoly π) RingHom (π βs (π΅ βm
1o))) β ((1o evalSub π)βπ
):(Baseβ(1o mPoly π))βΆ(Baseβ(π βs
(π΅ βm
1o)))) |
14 | 10, 13 | syl 17 |
. . . 4
β’ (π β ((1o evalSub
π)βπ
):(Baseβ(1o mPoly π))βΆ(Baseβ(π βs
(π΅ βm
1o)))) |
15 | | evls1sca.a |
. . . . . . 7
β’ π΄ = (algScβπ) |
16 | | eqid 2737 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
17 | 6 | subrgring 20241 |
. . . . . . . . 9
β’ (π
β (SubRingβπ) β π β Ring) |
18 | 3, 17 | syl 17 |
. . . . . . . 8
β’ (π β π β Ring) |
19 | | evls1sca.w |
. . . . . . . . 9
β’ π = (Poly1βπ) |
20 | 19 | ply1ring 21635 |
. . . . . . . 8
β’ (π β Ring β π β Ring) |
21 | 18, 20 | syl 17 |
. . . . . . 7
β’ (π β π β Ring) |
22 | 19 | ply1lmod 21639 |
. . . . . . . 8
β’ (π β Ring β π β LMod) |
23 | 18, 22 | syl 17 |
. . . . . . 7
β’ (π β π β LMod) |
24 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
25 | | eqid 2737 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
26 | 15, 16, 21, 23, 24, 25 | asclf 21301 |
. . . . . 6
β’ (π β π΄:(Baseβ(Scalarβπ))βΆ(Baseβπ)) |
27 | 8 | subrgss 20239 |
. . . . . . . . . 10
β’ (π
β (SubRingβπ) β π
β π΅) |
28 | 3, 27 | syl 17 |
. . . . . . . . 9
β’ (π β π
β π΅) |
29 | 6, 8 | ressbas2 17127 |
. . . . . . . . 9
β’ (π
β π΅ β π
= (Baseβπ)) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
β’ (π β π
= (Baseβπ)) |
31 | 19 | ply1sca 21640 |
. . . . . . . . . 10
β’ (π β Ring β π = (Scalarβπ)) |
32 | 18, 31 | syl 17 |
. . . . . . . . 9
β’ (π β π = (Scalarβπ)) |
33 | 32 | fveq2d 6851 |
. . . . . . . 8
β’ (π β (Baseβπ) =
(Baseβ(Scalarβπ))) |
34 | 30, 33 | eqtrd 2777 |
. . . . . . 7
β’ (π β π
= (Baseβ(Scalarβπ))) |
35 | | eqid 2737 |
. . . . . . . . . 10
β’
(PwSer1βπ) = (PwSer1βπ) |
36 | 19, 35, 25 | ply1bas 21582 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβ(1o mPoly π)) |
37 | 36 | a1i 11 |
. . . . . . . 8
β’ (π β (Baseβπ) = (Baseβ(1o
mPoly π))) |
38 | 37 | eqcomd 2743 |
. . . . . . 7
β’ (π β (Baseβ(1o
mPoly π)) =
(Baseβπ)) |
39 | 34, 38 | feq23d 6668 |
. . . . . 6
β’ (π β (π΄:π
βΆ(Baseβ(1o mPoly
π)) β π΄:(Baseβ(Scalarβπ))βΆ(Baseβπ))) |
40 | 26, 39 | mpbird 257 |
. . . . 5
β’ (π β π΄:π
βΆ(Baseβ(1o mPoly
π))) |
41 | | evls1sca.x |
. . . . 5
β’ (π β π β π
) |
42 | 40, 41 | ffvelcdmd 7041 |
. . . 4
β’ (π β (π΄βπ) β (Baseβ(1o mPoly
π))) |
43 | | fvco3 6945 |
. . . 4
β’
((((1o evalSub π)βπ
):(Baseβ(1o mPoly π))βΆ(Baseβ(π βs
(π΅ βm
1o))) β§ (π΄βπ) β (Baseβ(1o mPoly
π))) β (((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β ((1o
evalSub π)βπ
))β(π΄βπ)) = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))β(((1o
evalSub π)βπ
)β(π΄βπ)))) |
44 | 14, 42, 43 | syl2anc 585 |
. . 3
β’ (π β (((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β ((1o
evalSub π)βπ
))β(π΄βπ)) = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))β(((1o
evalSub π)βπ
)β(π΄βπ)))) |
45 | 15 | a1i 11 |
. . . . . . . 8
β’ (π β π΄ = (algScβπ)) |
46 | | eqid 2737 |
. . . . . . . . 9
β’
(algScβπ) =
(algScβπ) |
47 | 19, 46 | ply1ascl 21645 |
. . . . . . . 8
β’
(algScβπ) =
(algScβ(1o mPoly π)) |
48 | 45, 47 | eqtrdi 2793 |
. . . . . . 7
β’ (π β π΄ = (algScβ(1o mPoly π))) |
49 | 48 | fveq1d 6849 |
. . . . . 6
β’ (π β (π΄βπ) = ((algScβ(1o mPoly π))βπ)) |
50 | 49 | fveq2d 6851 |
. . . . 5
β’ (π β (((1o evalSub
π)βπ
)β(π΄βπ)) = (((1o evalSub π)βπ
)β((algScβ(1o mPoly
π))βπ))) |
51 | | eqid 2737 |
. . . . . 6
β’
(algScβ(1o mPoly π)) = (algScβ(1o mPoly π)) |
52 | 1 | a1i 11 |
. . . . . 6
β’ (π β 1o β
On) |
53 | 4, 5, 6, 8, 51, 52, 2, 3, 41 | evlssca 21515 |
. . . . 5
β’ (π β (((1o evalSub
π)βπ
)β((algScβ(1o mPoly
π))βπ)) = ((π΅ βm 1o) Γ
{π})) |
54 | 50, 53 | eqtrd 2777 |
. . . 4
β’ (π β (((1o evalSub
π)βπ
)β(π΄βπ)) = ((π΅ βm 1o) Γ
{π})) |
55 | 54 | fveq2d 6851 |
. . 3
β’ (π β ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))β(((1o
evalSub π)βπ
)β(π΄βπ))) = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))β((π΅ βm 1o) Γ
{π}))) |
56 | | eqidd 2738 |
. . . . 5
β’ (π β (π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) = (π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))) |
57 | | coeq1 5818 |
. . . . . 6
β’ (π₯ = ((π΅ βm 1o) Γ
{π}) β (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
58 | 57 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ = ((π΅ βm 1o) Γ
{π})) β (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
59 | 28, 41 | sseldd 3950 |
. . . . . . 7
β’ (π β π β π΅) |
60 | | fconst6g 6736 |
. . . . . . 7
β’ (π β π΅ β ((π΅ βm 1o) Γ
{π}):(π΅ βm
1o)βΆπ΅) |
61 | 59, 60 | syl 17 |
. . . . . 6
β’ (π β ((π΅ βm 1o) Γ
{π}):(π΅ βm
1o)βΆπ΅) |
62 | 8 | fvexi 6861 |
. . . . . . . 8
β’ π΅ β V |
63 | 62 | a1i 11 |
. . . . . . 7
β’ (π β π΅ β V) |
64 | | ovex 7395 |
. . . . . . . 8
β’ (π΅ βm
1o) β V |
65 | 64 | a1i 11 |
. . . . . . 7
β’ (π β (π΅ βm 1o) β
V) |
66 | 63, 65 | elmapd 8786 |
. . . . . 6
β’ (π β (((π΅ βm 1o) Γ
{π}) β (π΅ βm (π΅ βm
1o)) β ((π΅
βm 1o) Γ {π}):(π΅ βm
1o)βΆπ΅)) |
67 | 61, 66 | mpbird 257 |
. . . . 5
β’ (π β ((π΅ βm 1o) Γ
{π}) β (π΅ βm (π΅ βm
1o))) |
68 | | snex 5393 |
. . . . . . . 8
β’ {π} β V |
69 | 64, 68 | xpex 7692 |
. . . . . . 7
β’ ((π΅ βm
1o) Γ {π})
β V |
70 | 69 | a1i 11 |
. . . . . 6
β’ (π β ((π΅ βm 1o) Γ
{π}) β
V) |
71 | 63 | mptexd 7179 |
. . . . . 6
β’ (π β (π¦ β π΅ β¦ (1o Γ {π¦})) β V) |
72 | | coexg 7871 |
. . . . . 6
β’ ((((π΅ βm
1o) Γ {π})
β V β§ (π¦ β
π΅ β¦ (1o
Γ {π¦})) β V)
β (((π΅
βm 1o) Γ {π}) β (π¦ β π΅ β¦ (1o Γ {π¦}))) β V) |
73 | 70, 71, 72 | syl2anc 585 |
. . . . 5
β’ (π β (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦}))) β V) |
74 | 56, 58, 67, 73 | fvmptd 6960 |
. . . 4
β’ (π β ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))β((π΅ βm 1o) Γ
{π})) = (((π΅ βm
1o) Γ {π})
β (π¦ β π΅ β¦ (1o Γ
{π¦})))) |
75 | | fconst6g 6736 |
. . . . . . 7
β’ (π¦ β π΅ β (1o Γ {π¦}):1oβΆπ΅) |
76 | 75 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β (1o Γ {π¦}):1oβΆπ΅) |
77 | 62, 1 | pm3.2i 472 |
. . . . . . . 8
β’ (π΅ β V β§ 1o
β On) |
78 | 77 | a1i 11 |
. . . . . . 7
β’ ((π β§ π¦ β π΅) β (π΅ β V β§ 1o β
On)) |
79 | | elmapg 8785 |
. . . . . . 7
β’ ((π΅ β V β§ 1o
β On) β ((1o Γ {π¦}) β (π΅ βm 1o) β
(1o Γ {π¦}):1oβΆπ΅)) |
80 | 78, 79 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β ((1o Γ {π¦}) β (π΅ βm 1o) β
(1o Γ {π¦}):1oβΆπ΅)) |
81 | 76, 80 | mpbird 257 |
. . . . 5
β’ ((π β§ π¦ β π΅) β (1o Γ {π¦}) β (π΅ βm
1o)) |
82 | | eqidd 2738 |
. . . . 5
β’ (π β (π¦ β π΅ β¦ (1o Γ {π¦})) = (π¦ β π΅ β¦ (1o Γ {π¦}))) |
83 | | fconstmpt 5699 |
. . . . . 6
β’ ((π΅ βm
1o) Γ {π})
= (π§ β (π΅ βm
1o) β¦ π) |
84 | 83 | a1i 11 |
. . . . 5
β’ (π β ((π΅ βm 1o) Γ
{π}) = (π§ β (π΅ βm 1o) β¦
π)) |
85 | | eqidd 2738 |
. . . . 5
β’ (π§ = (1o Γ {π¦}) β π = π) |
86 | 81, 82, 84, 85 | fmptco 7080 |
. . . 4
β’ (π β (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (π¦ β π΅ β¦ π)) |
87 | 74, 86 | eqtrd 2777 |
. . 3
β’ (π β ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦}))))β((π΅ βm 1o) Γ
{π})) = (π¦ β π΅ β¦ π)) |
88 | 44, 55, 87 | 3eqtrd 2781 |
. 2
β’ (π β (((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β ((1o
evalSub π)βπ
))β(π΄βπ)) = (π¦ β π΅ β¦ π)) |
89 | | elpwg 4568 |
. . . . . 6
β’ (π
β (SubRingβπ) β (π
β π« π΅ β π
β π΅)) |
90 | 27, 89 | mpbird 257 |
. . . . 5
β’ (π
β (SubRingβπ) β π
β π« π΅) |
91 | 3, 90 | syl 17 |
. . . 4
β’ (π β π
β π« π΅) |
92 | | evls1sca.q |
. . . . 5
β’ π = (π evalSub1 π
) |
93 | | eqid 2737 |
. . . . 5
β’
(1o evalSub π) = (1o evalSub π) |
94 | 92, 93, 8 | evls1fval 21701 |
. . . 4
β’ ((π β CRing β§ π
β π« π΅) β π = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β ((1o
evalSub π)βπ
))) |
95 | 2, 91, 94 | syl2anc 585 |
. . 3
β’ (π β π = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β ((1o
evalSub π)βπ
))) |
96 | 95 | fveq1d 6849 |
. 2
β’ (π β (πβ(π΄βπ)) = (((π₯ β (π΅ βm (π΅ βm 1o)) β¦
(π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β ((1o
evalSub π)βπ
))β(π΄βπ))) |
97 | | fconstmpt 5699 |
. . 3
β’ (π΅ Γ {π}) = (π¦ β π΅ β¦ π) |
98 | 97 | a1i 11 |
. 2
β’ (π β (π΅ Γ {π}) = (π¦ β π΅ β¦ π)) |
99 | 88, 96, 98 | 3eqtr4d 2787 |
1
β’ (π β (πβ(π΄βπ)) = (π΅ Γ {π})) |