Step | Hyp | Ref
| Expression |
1 | | mpfpf1.q |
. . . . 5
β’ πΈ = ran (1o eval π
) |
2 | | eqid 2737 |
. . . . . . 7
β’
(1o eval π
) = (1o eval π
) |
3 | | pf1f.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
4 | 2, 3 | evlval 21521 |
. . . . . 6
β’
(1o eval π
) = ((1o evalSub π
)βπ΅) |
5 | 4 | rneqi 5897 |
. . . . 5
β’ ran
(1o eval π
) =
ran ((1o evalSub π
)βπ΅) |
6 | 1, 5 | eqtri 2765 |
. . . 4
β’ πΈ = ran ((1o evalSub
π
)βπ΅) |
7 | 6 | mpfrcl 21511 |
. . 3
β’ (πΉ β πΈ β (1o β V β§ π
β CRing β§ π΅ β (SubRingβπ
))) |
8 | 7 | simp2d 1144 |
. 2
β’ (πΉ β πΈ β π
β CRing) |
9 | | id 22 |
. . . 4
β’ (πΉ β πΈ β πΉ β πΈ) |
10 | 9, 1 | eleqtrdi 2848 |
. . 3
β’ (πΉ β πΈ β πΉ β ran (1o eval π
)) |
11 | | 1on 8429 |
. . . . 5
β’
1o β On |
12 | | eqid 2737 |
. . . . . 6
β’
(1o mPoly π
) = (1o mPoly π
) |
13 | | eqid 2737 |
. . . . . 6
β’ (π
βs
(π΅ βm
1o)) = (π
βs (π΅ βm
1o)) |
14 | 2, 3, 12, 13 | evlrhm 21522 |
. . . . 5
β’
((1o β On β§ π
β CRing) β (1o eval
π
) β ((1o
mPoly π
) RingHom (π
βs
(π΅ βm
1o)))) |
15 | 11, 8, 14 | sylancr 588 |
. . . 4
β’ (πΉ β πΈ β (1o eval π
) β ((1o mPoly
π
) RingHom (π
βs
(π΅ βm
1o)))) |
16 | | eqid 2737 |
. . . . . 6
β’
(Poly1βπ
) = (Poly1βπ
) |
17 | | eqid 2737 |
. . . . . 6
β’
(PwSer1βπ
) = (PwSer1βπ
) |
18 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(Poly1βπ
)) =
(Baseβ(Poly1βπ
)) |
19 | 16, 17, 18 | ply1bas 21582 |
. . . . 5
β’
(Baseβ(Poly1βπ
)) = (Baseβ(1o mPoly π
)) |
20 | | eqid 2737 |
. . . . 5
β’
(Baseβ(π
βs (π΅ βm 1o))) =
(Baseβ(π
βs (π΅ βm
1o))) |
21 | 19, 20 | rhmf 20167 |
. . . 4
β’
((1o eval π
) β ((1o mPoly π
) RingHom (π
βs (π΅ βm
1o))) β (1o eval π
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs
(π΅ βm
1o)))) |
22 | | ffn 6673 |
. . . 4
β’
((1o eval π
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs
(π΅ βm
1o))) β (1o eval π
) Fn
(Baseβ(Poly1βπ
))) |
23 | | fvelrnb 6908 |
. . . 4
β’
((1o eval π
) Fn
(Baseβ(Poly1βπ
)) β (πΉ β ran (1o eval π
) β βπ₯ β
(Baseβ(Poly1βπ
))((1o eval π
)βπ₯) = πΉ)) |
24 | 15, 21, 22, 23 | 4syl 19 |
. . 3
β’ (πΉ β πΈ β (πΉ β ran (1o eval π
) β βπ₯ β
(Baseβ(Poly1βπ
))((1o eval π
)βπ₯) = πΉ)) |
25 | 10, 24 | mpbid 231 |
. 2
β’ (πΉ β πΈ β βπ₯ β
(Baseβ(Poly1βπ
))((1o eval π
)βπ₯) = πΉ) |
26 | | eqid 2737 |
. . . . . 6
β’
(eval1βπ
) = (eval1βπ
) |
27 | 26, 2, 3, 12, 19 | evl1val 21711 |
. . . . 5
β’ ((π
β CRing β§ π₯ β
(Baseβ(Poly1βπ
))) β ((eval1βπ
)βπ₯) = (((1o eval π
)βπ₯) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
28 | | eqid 2737 |
. . . . . . . . 9
β’ (π
βs π΅) = (π
βs π΅) |
29 | 26, 16, 28, 3 | evl1rhm 21714 |
. . . . . . . 8
β’ (π
β CRing β
(eval1βπ
)
β ((Poly1βπ
) RingHom (π
βs π΅))) |
30 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβ(π
βs π΅)) = (Baseβ(π
βs π΅)) |
31 | 18, 30 | rhmf 20167 |
. . . . . . . 8
β’
((eval1βπ
) β ((Poly1βπ
) RingHom (π
βs π΅)) β (eval1βπ
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs π΅))) |
32 | | ffn 6673 |
. . . . . . . 8
β’
((eval1βπ
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs π΅)) β
(eval1βπ
)
Fn (Baseβ(Poly1βπ
))) |
33 | 29, 31, 32 | 3syl 18 |
. . . . . . 7
β’ (π
β CRing β
(eval1βπ
)
Fn (Baseβ(Poly1βπ
))) |
34 | | fnfvelrn 7036 |
. . . . . . 7
β’
(((eval1βπ
) Fn
(Baseβ(Poly1βπ
)) β§ π₯ β
(Baseβ(Poly1βπ
))) β ((eval1βπ
)βπ₯) β ran (eval1βπ
)) |
35 | 33, 34 | sylan 581 |
. . . . . 6
β’ ((π
β CRing β§ π₯ β
(Baseβ(Poly1βπ
))) β ((eval1βπ
)βπ₯) β ran (eval1βπ
)) |
36 | | pf1rcl.q |
. . . . . 6
β’ π = ran
(eval1βπ
) |
37 | 35, 36 | eleqtrrdi 2849 |
. . . . 5
β’ ((π
β CRing β§ π₯ β
(Baseβ(Poly1βπ
))) β ((eval1βπ
)βπ₯) β π) |
38 | 27, 37 | eqeltrrd 2839 |
. . . 4
β’ ((π
β CRing β§ π₯ β
(Baseβ(Poly1βπ
))) β (((1o eval π
)βπ₯) β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π) |
39 | | coeq1 5818 |
. . . . 5
β’
(((1o eval π
)βπ₯) = πΉ β (((1o eval π
)βπ₯) β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
40 | 39 | eleq1d 2823 |
. . . 4
β’
(((1o eval π
)βπ₯) = πΉ β ((((1o eval π
)βπ₯) β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π)) |
41 | 38, 40 | syl5ibcom 244 |
. . 3
β’ ((π
β CRing β§ π₯ β
(Baseβ(Poly1βπ
))) β (((1o eval π
)βπ₯) = πΉ β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π)) |
42 | 41 | rexlimdva 3153 |
. 2
β’ (π
β CRing β
(βπ₯ β
(Baseβ(Poly1βπ
))((1o eval π
)βπ₯) = πΉ β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π)) |
43 | 8, 25, 42 | sylc 65 |
1
β’ (πΉ β πΈ β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π) |