Step | Hyp | Ref
| Expression |
1 | | crngring 19983 |
. . . . . 6
β’ (π
β CRing β π
β Ring) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β π
β Ring) |
3 | | evl1sca.p |
. . . . . 6
β’ π = (Poly1βπ
) |
4 | | evl1sca.a |
. . . . . 6
β’ π΄ = (algScβπ) |
5 | | evl1sca.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
6 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
7 | 3, 4, 5, 6 | ply1sclf 21672 |
. . . . 5
β’ (π
β Ring β π΄:π΅βΆ(Baseβπ)) |
8 | 2, 7 | syl 17 |
. . . 4
β’ ((π
β CRing β§ π β π΅) β π΄:π΅βΆ(Baseβπ)) |
9 | | ffvelcdm 7037 |
. . . 4
β’ ((π΄:π΅βΆ(Baseβπ) β§ π β π΅) β (π΄βπ) β (Baseβπ)) |
10 | 8, 9 | sylancom 589 |
. . 3
β’ ((π
β CRing β§ π β π΅) β (π΄βπ) β (Baseβπ)) |
11 | | evl1sca.o |
. . . 4
β’ π = (eval1βπ
) |
12 | | eqid 2737 |
. . . 4
β’
(1o eval π
) = (1o eval π
) |
13 | | eqid 2737 |
. . . 4
β’
(1o mPoly π
) = (1o mPoly π
) |
14 | | eqid 2737 |
. . . . 5
β’
(PwSer1βπ
) = (PwSer1βπ
) |
15 | 3, 14, 6 | ply1bas 21582 |
. . . 4
β’
(Baseβπ) =
(Baseβ(1o mPoly π
)) |
16 | 11, 12, 5, 13, 15 | evl1val 21711 |
. . 3
β’ ((π
β CRing β§ (π΄βπ) β (Baseβπ)) β (πβ(π΄βπ)) = (((1o eval π
)β(π΄βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
17 | 10, 16 | syldan 592 |
. 2
β’ ((π
β CRing β§ π β π΅) β (πβ(π΄βπ)) = (((1o eval π
)β(π΄βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
18 | 3, 4 | ply1ascl 21645 |
. . . . . . 7
β’ π΄ = (algScβ(1o
mPoly π
)) |
19 | 5 | ressid 17132 |
. . . . . . . . . 10
β’ (π
β CRing β (π
βΎs π΅) = π
) |
20 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β π΅) β (π
βΎs π΅) = π
) |
21 | 20 | oveq2d 7378 |
. . . . . . . 8
β’ ((π
β CRing β§ π β π΅) β (1o mPoly (π
βΎs π΅)) = (1o mPoly π
)) |
22 | 21 | fveq2d 6851 |
. . . . . . 7
β’ ((π
β CRing β§ π β π΅) β (algScβ(1o mPoly
(π
βΎs
π΅))) =
(algScβ(1o mPoly π
))) |
23 | 18, 22 | eqtr4id 2796 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅) β π΄ = (algScβ(1o mPoly (π
βΎs π΅)))) |
24 | 23 | fveq1d 6849 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β (π΄βπ) = ((algScβ(1o mPoly
(π
βΎs
π΅)))βπ)) |
25 | 24 | fveq2d 6851 |
. . . 4
β’ ((π
β CRing β§ π β π΅) β ((1o eval π
)β(π΄βπ)) = ((1o eval π
)β((algScβ(1o mPoly
(π
βΎs
π΅)))βπ))) |
26 | 12, 5 | evlval 21521 |
. . . . 5
β’
(1o eval π
) = ((1o evalSub π
)βπ΅) |
27 | | eqid 2737 |
. . . . 5
β’
(1o mPoly (π
βΎs π΅)) = (1o mPoly (π
βΎs π΅)) |
28 | | eqid 2737 |
. . . . 5
β’ (π
βΎs π΅) = (π
βΎs π΅) |
29 | | eqid 2737 |
. . . . 5
β’
(algScβ(1o mPoly (π
βΎs π΅))) = (algScβ(1o mPoly
(π
βΎs
π΅))) |
30 | | 1on 8429 |
. . . . . 6
β’
1o β On |
31 | 30 | a1i 11 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β 1o β
On) |
32 | | simpl 484 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β π
β CRing) |
33 | 5 | subrgid 20240 |
. . . . . 6
β’ (π
β Ring β π΅ β (SubRingβπ
)) |
34 | 2, 33 | syl 17 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β π΅ β (SubRingβπ
)) |
35 | | simpr 486 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β π β π΅) |
36 | 26, 27, 28, 5, 29, 31, 32, 34, 35 | evlssca 21515 |
. . . 4
β’ ((π
β CRing β§ π β π΅) β ((1o eval π
)β((algScβ(1o mPoly
(π
βΎs
π΅)))βπ)) = ((π΅ βm 1o) Γ
{π})) |
37 | 25, 36 | eqtrd 2777 |
. . 3
β’ ((π
β CRing β§ π β π΅) β ((1o eval π
)β(π΄βπ)) = ((π΅ βm 1o) Γ
{π})) |
38 | 37 | coeq1d 5822 |
. 2
β’ ((π
β CRing β§ π β π΅) β (((1o eval π
)β(π΄βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
39 | | df1o2 8424 |
. . . . . . 7
β’
1o = {β
} |
40 | 5 | fvexi 6861 |
. . . . . . 7
β’ π΅ β V |
41 | | 0ex 5269 |
. . . . . . 7
β’ β
β V |
42 | | eqid 2737 |
. . . . . . 7
β’ (π¦ β π΅ β¦ (1o Γ {π¦})) = (π¦ β π΅ β¦ (1o Γ {π¦})) |
43 | 39, 40, 41, 42 | mapsnf1o3 8840 |
. . . . . 6
β’ (π¦ β π΅ β¦ (1o Γ {π¦})):π΅β1-1-ontoβ(π΅ βm
1o) |
44 | | f1of 6789 |
. . . . . 6
β’ ((π¦ β π΅ β¦ (1o Γ {π¦})):π΅β1-1-ontoβ(π΅ βm 1o) β
(π¦ β π΅ β¦ (1o Γ {π¦})):π΅βΆ(π΅ βm
1o)) |
45 | 43, 44 | mp1i 13 |
. . . . 5
β’ ((π
β CRing β§ π β π΅) β (π¦ β π΅ β¦ (1o Γ {π¦})):π΅βΆ(π΅ βm
1o)) |
46 | 42 | fmpt 7063 |
. . . . 5
β’
(βπ¦ β
π΅ (1o Γ
{π¦}) β (π΅ βm
1o) β (π¦
β π΅ β¦
(1o Γ {π¦})):π΅βΆ(π΅ βm
1o)) |
47 | 45, 46 | sylibr 233 |
. . . 4
β’ ((π
β CRing β§ π β π΅) β βπ¦ β π΅ (1o Γ {π¦}) β (π΅ βm
1o)) |
48 | | eqidd 2738 |
. . . 4
β’ ((π
β CRing β§ π β π΅) β (π¦ β π΅ β¦ (1o Γ {π¦})) = (π¦ β π΅ β¦ (1o Γ {π¦}))) |
49 | | fconstmpt 5699 |
. . . . 5
β’ ((π΅ βm
1o) Γ {π})
= (π₯ β (π΅ βm
1o) β¦ π) |
50 | 49 | a1i 11 |
. . . 4
β’ ((π
β CRing β§ π β π΅) β ((π΅ βm 1o) Γ
{π}) = (π₯ β (π΅ βm 1o) β¦
π)) |
51 | | eqidd 2738 |
. . . 4
β’ (π₯ = (1o Γ {π¦}) β π = π) |
52 | 47, 48, 50, 51 | fmptcof 7081 |
. . 3
β’ ((π
β CRing β§ π β π΅) β (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (π¦ β π΅ β¦ π)) |
53 | | fconstmpt 5699 |
. . 3
β’ (π΅ Γ {π}) = (π¦ β π΅ β¦ π) |
54 | 52, 53 | eqtr4di 2795 |
. 2
β’ ((π
β CRing β§ π β π΅) β (((π΅ βm 1o) Γ
{π}) β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (π΅ Γ {π})) |
55 | 17, 38, 54 | 3eqtrd 2781 |
1
β’ ((π
β CRing β§ π β π΅) β (πβ(π΄βπ)) = (π΅ Γ {π})) |