Step | Hyp | Ref
| Expression |
1 | | evlsval3.i |
. . 3
β’ (π β πΌ β π) |
2 | | evlsval3.s |
. . 3
β’ (π β π β CRing) |
3 | | evlsval3.r |
. . 3
β’ (π β π
β (SubRingβπ)) |
4 | | evlsval3.q |
. . . 4
β’ π = ((πΌ evalSub π)βπ
) |
5 | | evlsval3.p |
. . . 4
β’ π = (πΌ mPoly π) |
6 | | eqid 2733 |
. . . 4
β’ (πΌ mVar π) = (πΌ mVar π) |
7 | | evlsval3.u |
. . . 4
β’ π = (π βΎs π
) |
8 | | evlsval3.t |
. . . 4
β’ π = (π βs (πΎ βm πΌ)) |
9 | | evlsval3.k |
. . . 4
β’ πΎ = (Baseβπ) |
10 | | eqid 2733 |
. . . 4
β’
(algScβπ) =
(algScβπ) |
11 | | evlsval3.f |
. . . 4
β’ πΉ = (π₯ β π
β¦ ((πΎ βm πΌ) Γ {π₯})) |
12 | | evlsval3.g |
. . . 4
β’ πΊ = (π₯ β πΌ β¦ (π β (πΎ βm πΌ) β¦ (πβπ₯))) |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | evlsval 21519 |
. . 3
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π = (β©π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ))) |
14 | 1, 2, 3, 13 | syl3anc 1372 |
. 2
β’ (π β π = (β©π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ))) |
15 | | evlsval3.b |
. . . . 5
β’ π΅ = (Baseβπ) |
16 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
17 | | evlsval3.d |
. . . . 5
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
18 | | evlsval3.m |
. . . . 5
β’ π = (mulGrpβπ) |
19 | | evlsval3.w |
. . . . 5
β’ β =
(.gβπ) |
20 | | evlsval3.x |
. . . . 5
β’ Β· =
(.rβπ) |
21 | | evlsval3.e |
. . . . 5
β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
22 | 7 | subrgcrng 20268 |
. . . . . 6
β’ ((π β CRing β§ π
β (SubRingβπ)) β π β CRing) |
23 | 2, 3, 22 | syl2anc 585 |
. . . . 5
β’ (π β π β CRing) |
24 | | ovexd 7396 |
. . . . . 6
β’ (π β (πΎ βm πΌ) β V) |
25 | 8 | pwscrng 20049 |
. . . . . 6
β’ ((π β CRing β§ (πΎ βm πΌ) β V) β π β CRing) |
26 | 2, 24, 25 | syl2anc 585 |
. . . . 5
β’ (π β π β CRing) |
27 | 9 | subrgss 20265 |
. . . . . . . . 9
β’ (π
β (SubRingβπ) β π
β πΎ) |
28 | 3, 27 | syl 17 |
. . . . . . . 8
β’ (π β π
β πΎ) |
29 | 28 | resmptd 5998 |
. . . . . . 7
β’ (π β ((π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) βΎ π
) = (π₯ β π
β¦ ((πΎ βm πΌ) Γ {π₯}))) |
30 | 11, 29 | eqtr4id 2792 |
. . . . . 6
β’ (π β πΉ = ((π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) βΎ π
)) |
31 | 2 | crngringd 19985 |
. . . . . . . 8
β’ (π β π β Ring) |
32 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) = (π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) |
33 | 8, 9, 32 | pwsdiagrhm 20299 |
. . . . . . . 8
β’ ((π β Ring β§ (πΎ βm πΌ) β V) β (π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) β (π RingHom π)) |
34 | 31, 24, 33 | syl2anc 585 |
. . . . . . 7
β’ (π β (π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) β (π RingHom π)) |
35 | 7 | resrhm 20294 |
. . . . . . 7
β’ (((π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) β (π RingHom π) β§ π
β (SubRingβπ)) β ((π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) βΎ π
) β (π RingHom π)) |
36 | 34, 3, 35 | syl2anc 585 |
. . . . . 6
β’ (π β ((π₯ β πΎ β¦ ((πΎ βm πΌ) Γ {π₯})) βΎ π
) β (π RingHom π)) |
37 | 30, 36 | eqeltrd 2834 |
. . . . 5
β’ (π β πΉ β (π RingHom π)) |
38 | 9 | fvexi 6860 |
. . . . . . . . . . . 12
β’ πΎ β V |
39 | | elmapg 8784 |
. . . . . . . . . . . 12
β’ ((πΎ β V β§ πΌ β π) β (π β (πΎ βm πΌ) β π:πΌβΆπΎ)) |
40 | 38, 1, 39 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (π β (πΎ βm πΌ) β π:πΌβΆπΎ)) |
41 | 40 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ π β (πΎ βm πΌ)) β π:πΌβΆπΎ) |
42 | 41 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΌ) β§ π β (πΎ βm πΌ)) β π:πΌβΆπΎ) |
43 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΌ) β§ π β (πΎ βm πΌ)) β π₯ β πΌ) |
44 | 42, 43 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (((π β§ π₯ β πΌ) β§ π β (πΎ βm πΌ)) β (πβπ₯) β πΎ) |
45 | 44 | fmpttd 7067 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (π β (πΎ βm πΌ) β¦ (πβπ₯)):(πΎ βm πΌ)βΆπΎ) |
46 | | ovexd 7396 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β (πΎ βm πΌ) β V) |
47 | 8, 9, 16 | pwselbasb 17378 |
. . . . . . . 8
β’ ((π β CRing β§ (πΎ βm πΌ) β V) β ((π β (πΎ βm πΌ) β¦ (πβπ₯)) β (Baseβπ) β (π β (πΎ βm πΌ) β¦ (πβπ₯)):(πΎ βm πΌ)βΆπΎ)) |
48 | 2, 46, 47 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β ((π β (πΎ βm πΌ) β¦ (πβπ₯)) β (Baseβπ) β (π β (πΎ βm πΌ) β¦ (πβπ₯)):(πΎ βm πΌ)βΆπΎ)) |
49 | 45, 48 | mpbird 257 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (π β (πΎ βm πΌ) β¦ (πβπ₯)) β (Baseβπ)) |
50 | 49, 12 | fmptd 7066 |
. . . . 5
β’ (π β πΊ:πΌβΆ(Baseβπ)) |
51 | 5, 15, 16, 17, 18, 19, 20, 6, 21, 1, 23, 26, 37, 50, 10 | evlslem1 21515 |
. . . 4
β’ (π β (πΈ β (π RingHom π) β§ (πΈ β (algScβπ)) = πΉ β§ (πΈ β (πΌ mVar π)) = πΊ)) |
52 | 51 | simp2d 1144 |
. . 3
β’ (π β (πΈ β (algScβπ)) = πΉ) |
53 | 51 | simp3d 1145 |
. . 3
β’ (π β (πΈ β (πΌ mVar π)) = πΊ) |
54 | 51 | simp1d 1143 |
. . . 4
β’ (π β πΈ β (π RingHom π)) |
55 | 5, 16, 10, 6, 1, 23, 26, 37, 50 | evlseu 21516 |
. . . 4
β’ (π β β!π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ)) |
56 | | coeq1 5817 |
. . . . . . 7
β’ (π = πΈ β (π β (algScβπ)) = (πΈ β (algScβπ))) |
57 | 56 | eqeq1d 2735 |
. . . . . 6
β’ (π = πΈ β ((π β (algScβπ)) = πΉ β (πΈ β (algScβπ)) = πΉ)) |
58 | | coeq1 5817 |
. . . . . . 7
β’ (π = πΈ β (π β (πΌ mVar π)) = (πΈ β (πΌ mVar π))) |
59 | 58 | eqeq1d 2735 |
. . . . . 6
β’ (π = πΈ β ((π β (πΌ mVar π)) = πΊ β (πΈ β (πΌ mVar π)) = πΊ)) |
60 | 57, 59 | anbi12d 632 |
. . . . 5
β’ (π = πΈ β (((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ) β ((πΈ β (algScβπ)) = πΉ β§ (πΈ β (πΌ mVar π)) = πΊ))) |
61 | 60 | riota2 7343 |
. . . 4
β’ ((πΈ β (π RingHom π) β§ β!π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ)) β (((πΈ β (algScβπ)) = πΉ β§ (πΈ β (πΌ mVar π)) = πΊ) β (β©π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ)) = πΈ)) |
62 | 54, 55, 61 | syl2anc 585 |
. . 3
β’ (π β (((πΈ β (algScβπ)) = πΉ β§ (πΈ β (πΌ mVar π)) = πΊ) β (β©π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ)) = πΈ)) |
63 | 52, 53, 62 | mpbi2and 711 |
. 2
β’ (π β (β©π β (π RingHom π)((π β (algScβπ)) = πΉ β§ (π β (πΌ mVar π)) = πΊ)) = πΈ) |
64 | 14, 63 | eqtrd 2773 |
1
β’ (π β π = πΈ) |