Step | Hyp | Ref
| Expression |
1 | | evlsval.q |
. . . 4
β’ π = ((πΌ evalSub π)βπ
) |
2 | | evlsval.w |
. . . 4
β’ π = (πΌ mPoly π) |
3 | | evlsval.v |
. . . 4
β’ π = (πΌ mVar π) |
4 | | evlsval.u |
. . . 4
β’ π = (π βΎs π
) |
5 | | evlsval.t |
. . . 4
β’ π = (π βs (π΅ βm πΌ)) |
6 | | evlsval.b |
. . . 4
β’ π΅ = (Baseβπ) |
7 | | evlsval.a |
. . . 4
β’ π΄ = (algScβπ) |
8 | | evlsval.x |
. . . 4
β’ π = (π₯ β π
β¦ ((π΅ βm πΌ) Γ {π₯})) |
9 | | evlsval.y |
. . . 4
β’ π = (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | evlsval 21640 |
. . 3
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π = (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π))) |
11 | | eqid 2732 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
12 | | simp1 1136 |
. . . . 5
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β πΌ β π) |
13 | 4 | subrgcrng 20359 |
. . . . . 6
β’ ((π β CRing β§ π
β (SubRingβπ)) β π β CRing) |
14 | 13 | 3adant1 1130 |
. . . . 5
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π β CRing) |
15 | | simp2 1137 |
. . . . . 6
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π β CRing) |
16 | | ovex 7438 |
. . . . . 6
β’ (π΅ βm πΌ) β V |
17 | 5 | pwscrng 20132 |
. . . . . 6
β’ ((π β CRing β§ (π΅ βm πΌ) β V) β π β CRing) |
18 | 15, 16, 17 | sylancl 586 |
. . . . 5
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π β CRing) |
19 | 6 | subrgss 20356 |
. . . . . . . . 9
β’ (π
β (SubRingβπ) β π
β π΅) |
20 | 19 | 3ad2ant3 1135 |
. . . . . . . 8
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π
β π΅) |
21 | 20 | resmptd 6038 |
. . . . . . 7
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β ((π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) βΎ π
) = (π₯ β π
β¦ ((π΅ βm πΌ) Γ {π₯}))) |
22 | 21, 8 | eqtr4di 2790 |
. . . . . 6
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β ((π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) βΎ π
) = π) |
23 | | crngring 20061 |
. . . . . . . . 9
β’ (π β CRing β π β Ring) |
24 | 23 | 3ad2ant2 1134 |
. . . . . . . 8
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π β Ring) |
25 | | eqid 2732 |
. . . . . . . . 9
β’ (π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) = (π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) |
26 | 5, 6, 25 | pwsdiagrhm 20391 |
. . . . . . . 8
β’ ((π β Ring β§ (π΅ βm πΌ) β V) β (π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) β (π RingHom π)) |
27 | 24, 16, 26 | sylancl 586 |
. . . . . . 7
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β (π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) β (π RingHom π)) |
28 | | simp3 1138 |
. . . . . . 7
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π
β (SubRingβπ)) |
29 | 4 | resrhm 20385 |
. . . . . . 7
β’ (((π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) β (π RingHom π) β§ π
β (SubRingβπ)) β ((π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) βΎ π
) β (π RingHom π)) |
30 | 27, 28, 29 | syl2anc 584 |
. . . . . 6
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β ((π₯ β π΅ β¦ ((π΅ βm πΌ) Γ {π₯})) βΎ π
) β (π RingHom π)) |
31 | 22, 30 | eqeltrrd 2834 |
. . . . 5
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π β (π RingHom π)) |
32 | 6 | fvexi 6902 |
. . . . . . . . . . 11
β’ π΅ β V |
33 | | simpl1 1191 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β πΌ β π) |
34 | | elmapg 8829 |
. . . . . . . . . . 11
β’ ((π΅ β V β§ πΌ β π) β (π β (π΅ βm πΌ) β π:πΌβΆπ΅)) |
35 | 32, 33, 34 | sylancr 587 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β (π β (π΅ βm πΌ) β π:πΌβΆπ΅)) |
36 | 35 | biimpa 477 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β§ π β (π΅ βm πΌ)) β π:πΌβΆπ΅) |
37 | | simplr 767 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β§ π β (π΅ βm πΌ)) β π₯ β πΌ) |
38 | 36, 37 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β§ π β (π΅ βm πΌ)) β (πβπ₯) β π΅) |
39 | 38 | fmpttd 7111 |
. . . . . . 7
β’ (((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β (π β (π΅ βm πΌ) β¦ (πβπ₯)):(π΅ βm πΌ)βΆπ΅) |
40 | | simpl2 1192 |
. . . . . . . 8
β’ (((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β π β CRing) |
41 | 5, 6, 11 | pwselbasb 17430 |
. . . . . . . 8
β’ ((π β CRing β§ (π΅ βm πΌ) β V) β ((π β (π΅ βm πΌ) β¦ (πβπ₯)) β (Baseβπ) β (π β (π΅ βm πΌ) β¦ (πβπ₯)):(π΅ βm πΌ)βΆπ΅)) |
42 | 40, 16, 41 | sylancl 586 |
. . . . . . 7
β’ (((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β ((π β (π΅ βm πΌ) β¦ (πβπ₯)) β (Baseβπ) β (π β (π΅ βm πΌ) β¦ (πβπ₯)):(π΅ βm πΌ)βΆπ΅)) |
43 | 39, 42 | mpbird 256 |
. . . . . 6
β’ (((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β§ π₯ β πΌ) β (π β (π΅ βm πΌ) β¦ (πβπ₯)) β (Baseβπ)) |
44 | 43, 9 | fmptd 7110 |
. . . . 5
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π:πΌβΆ(Baseβπ)) |
45 | 2, 11, 7, 3, 12, 14, 18, 31, 44 | evlseu 21637 |
. . . 4
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β β!π β (π RingHom π)((π β π΄) = π β§ (π β π) = π)) |
46 | | riotacl2 7378 |
. . . 4
β’
(β!π β
(π RingHom π)((π β π΄) = π β§ (π β π) = π) β (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π)) β {π β (π RingHom π) β£ ((π β π΄) = π β§ (π β π) = π)}) |
47 | 45, 46 | syl 17 |
. . 3
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π)) β {π β (π RingHom π) β£ ((π β π΄) = π β§ (π β π) = π)}) |
48 | 10, 47 | eqeltrd 2833 |
. 2
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π β {π β (π RingHom π) β£ ((π β π΄) = π β§ (π β π) = π)}) |
49 | | coeq1 5855 |
. . . . 5
β’ (π = π β (π β π΄) = (π β π΄)) |
50 | 49 | eqeq1d 2734 |
. . . 4
β’ (π = π β ((π β π΄) = π β (π β π΄) = π)) |
51 | | coeq1 5855 |
. . . . 5
β’ (π = π β (π β π) = (π β π)) |
52 | 51 | eqeq1d 2734 |
. . . 4
β’ (π = π β ((π β π) = π β (π β π) = π)) |
53 | 50, 52 | anbi12d 631 |
. . 3
β’ (π = π β (((π β π΄) = π β§ (π β π) = π) β ((π β π΄) = π β§ (π β π) = π))) |
54 | 53 | elrab 3682 |
. 2
β’ (π β {π β (π RingHom π) β£ ((π β π΄) = π β§ (π β π) = π)} β (π β (π RingHom π) β§ ((π β π΄) = π β§ (π β π) = π))) |
55 | 48, 54 | sylib 217 |
1
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β (π β (π RingHom π) β§ ((π β π΄) = π β§ (π β π) = π))) |