Step | Hyp | Ref
| Expression |
1 | | mpfind.a |
. . . . 5
β’ (π β π΄ β π) |
2 | | mpfind.cq |
. . . . 5
β’ π = ran ((πΌ evalSub π)βπ
) |
3 | 1, 2 | eleqtrdi 2844 |
. . . 4
β’ (π β π΄ β ran ((πΌ evalSub π)βπ
)) |
4 | 2 | mpfrcl 21648 |
. . . . . . . 8
β’ (π΄ β π β (πΌ β V β§ π β CRing β§ π
β (SubRingβπ))) |
5 | 1, 4 | syl 17 |
. . . . . . 7
β’ (π β (πΌ β V β§ π β CRing β§ π
β (SubRingβπ))) |
6 | | eqid 2733 |
. . . . . . . 8
β’ ((πΌ evalSub π)βπ
) = ((πΌ evalSub π)βπ
) |
7 | | eqid 2733 |
. . . . . . . 8
β’ (πΌ mPoly (π βΎs π
)) = (πΌ mPoly (π βΎs π
)) |
8 | | eqid 2733 |
. . . . . . . 8
β’ (π βΎs π
) = (π βΎs π
) |
9 | | eqid 2733 |
. . . . . . . 8
β’ (π βs
(π΅ βm πΌ)) = (π βs (π΅ βm πΌ)) |
10 | | mpfind.cb |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
11 | 6, 7, 8, 9, 10 | evlsrhm 21651 |
. . . . . . 7
β’ ((πΌ β V β§ π β CRing β§ π
β (SubRingβπ)) β ((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ)))) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(πΌ mPoly
(π βΎs
π
))) = (Baseβ(πΌ mPoly (π βΎs π
))) |
13 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(π
βs (π΅ βm πΌ))) = (Baseβ(π βs (π΅ βm πΌ))) |
14 | 12, 13 | rhmf 20263 |
. . . . . . 7
β’ (((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ))) β ((πΌ evalSub π)βπ
):(Baseβ(πΌ mPoly (π βΎs π
)))βΆ(Baseβ(π βs (π΅ βm πΌ)))) |
15 | 5, 11, 14 | 3syl 18 |
. . . . . 6
β’ (π β ((πΌ evalSub π)βπ
):(Baseβ(πΌ mPoly (π βΎs π
)))βΆ(Baseβ(π βs (π΅ βm πΌ)))) |
16 | 15 | ffnd 6719 |
. . . . 5
β’ (π β ((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
)))) |
17 | | fvelrnb 6953 |
. . . . 5
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β (π΄ β ran ((πΌ evalSub π)βπ
) β βπ¦ β (Baseβ(πΌ mPoly (π βΎs π
)))(((πΌ evalSub π)βπ
)βπ¦) = π΄)) |
18 | 16, 17 | syl 17 |
. . . 4
β’ (π β (π΄ β ran ((πΌ evalSub π)βπ
) β βπ¦ β (Baseβ(πΌ mPoly (π βΎs π
)))(((πΌ evalSub π)βπ
)βπ¦) = π΄)) |
19 | 3, 18 | mpbid 231 |
. . 3
β’ (π β βπ¦ β (Baseβ(πΌ mPoly (π βΎs π
)))(((πΌ evalSub π)βπ
)βπ¦) = π΄) |
20 | 15 | ffund 6722 |
. . . . . 6
β’ (π β Fun ((πΌ evalSub π)βπ
)) |
21 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(π
βΎs π
)) =
(Baseβ(π
βΎs π
)) |
22 | | eqid 2733 |
. . . . . . 7
β’ (πΌ mVar (π βΎs π
)) = (πΌ mVar (π βΎs π
)) |
23 | | eqid 2733 |
. . . . . . 7
β’
(+gβ(πΌ mPoly (π βΎs π
))) = (+gβ(πΌ mPoly (π βΎs π
))) |
24 | | eqid 2733 |
. . . . . . 7
β’
(.rβ(πΌ mPoly (π βΎs π
))) = (.rβ(πΌ mPoly (π βΎs π
))) |
25 | | eqid 2733 |
. . . . . . 7
β’
(algScβ(πΌ
mPoly (π
βΎs π
))) =
(algScβ(πΌ mPoly
(π βΎs
π
))) |
26 | 5 | simp1d 1143 |
. . . . . . . . . . . 12
β’ (π β πΌ β V) |
27 | 5 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ (π β π β CRing) |
28 | 5 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ (π β π
β (SubRingβπ)) |
29 | 8 | subrgcrng 20323 |
. . . . . . . . . . . . . 14
β’ ((π β CRing β§ π
β (SubRingβπ)) β (π βΎs π
) β CRing) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (π βΎs π
) β CRing) |
31 | | crngring 20068 |
. . . . . . . . . . . . 13
β’ ((π βΎs π
) β CRing β (π βΎs π
) β Ring) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π βΎs π
) β Ring) |
33 | 7 | mplring 21578 |
. . . . . . . . . . . 12
β’ ((πΌ β V β§ (π βΎs π
) β Ring) β (πΌ mPoly (π βΎs π
)) β Ring) |
34 | 26, 32, 33 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΌ mPoly (π βΎs π
)) β Ring) |
35 | 34 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (πΌ mPoly (π βΎs π
)) β Ring) |
36 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
37 | | elpreima 7060 |
. . . . . . . . . . . . . 14
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
38 | 16, 37 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
39 | 38 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
40 | 36, 39 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
41 | 40 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β π β (Baseβ(πΌ mPoly (π βΎs π
)))) |
42 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
43 | | elpreima 7060 |
. . . . . . . . . . . . . 14
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
44 | 16, 43 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
45 | 44 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
46 | 42, 45 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
47 | 46 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β π β (Baseβ(πΌ mPoly (π βΎs π
)))) |
48 | 12, 23 | ringacl 20095 |
. . . . . . . . . 10
β’ (((πΌ mPoly (π βΎs π
)) β Ring β§ π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
)))) β (π(+gβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
49 | 35, 41, 47, 48 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π(+gβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
50 | | rhmghm 20262 |
. . . . . . . . . . . . . 14
β’ (((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ))) β ((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) GrpHom (π βs (π΅ βm πΌ)))) |
51 | 5, 11, 50 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) GrpHom (π βs (π΅ βm πΌ)))) |
52 | 51 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) GrpHom (π βs (π΅ βm πΌ)))) |
53 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(+gβ(π βs (π΅ βm πΌ))) =
(+gβ(π
βs (π΅ βm πΌ))) |
54 | 12, 23, 53 | ghmlin 19097 |
. . . . . . . . . . . 12
β’ ((((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) GrpHom (π βs (π΅ βm πΌ))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
)))) β (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) = ((((πΌ evalSub π)βπ
)βπ)(+gβ(π βs (π΅ βm πΌ)))(((πΌ evalSub π)βπ
)βπ))) |
55 | 52, 41, 47, 54 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) = ((((πΌ evalSub π)βπ
)βπ)(+gβ(π βs (π΅ βm πΌ)))(((πΌ evalSub π)βπ
)βπ))) |
56 | 27 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β π β CRing) |
57 | | ovexd 7444 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π΅ βm πΌ) β V) |
58 | 15 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((πΌ evalSub π)βπ
):(Baseβ(πΌ mPoly (π βΎs π
)))βΆ(Baseβ(π βs (π΅ βm πΌ)))) |
59 | 58, 41 | ffvelcdmd 7088 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β (Baseβ(π βs (π΅ βm πΌ)))) |
60 | 58, 47 | ffvelcdmd 7088 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β (Baseβ(π βs (π΅ βm πΌ)))) |
61 | | mpfind.cp |
. . . . . . . . . . . 12
β’ + =
(+gβπ) |
62 | 9, 13, 56, 57, 59, 60, 61, 53 | pwsplusgval 17436 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ)(+gβ(π βs (π΅ βm πΌ)))(((πΌ evalSub π)βπ
)βπ)) = ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ))) |
63 | 55, 62 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) = ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ))) |
64 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β π) |
65 | | fnfvelrn 7083 |
. . . . . . . . . . . . . 14
β’ ((((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
)))) β (((πΌ evalSub π)βπ
)βπ) β ran ((πΌ evalSub π)βπ
)) |
66 | 16, 41, 65 | syl2an2r 684 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β ran ((πΌ evalSub π)βπ
)) |
67 | 66, 2 | eleqtrrdi 2845 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β π) |
68 | | fvimacnvi 7054 |
. . . . . . . . . . . . 13
β’ ((Fun
((πΌ evalSub π)βπ
) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) |
69 | 20, 36, 68 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) |
70 | 67, 69 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
71 | | fnfvelrn 7083 |
. . . . . . . . . . . . . 14
β’ ((((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
)))) β (((πΌ evalSub π)βπ
)βπ) β ran ((πΌ evalSub π)βπ
)) |
72 | 16, 47, 71 | syl2an2r 684 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β ran ((πΌ evalSub π)βπ
)) |
73 | 72, 2 | eleqtrrdi 2845 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β π) |
74 | | fvimacnvi 7054 |
. . . . . . . . . . . . 13
β’ ((Fun
((πΌ evalSub π)βπ
) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) |
75 | 20, 42, 74 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) |
76 | 73, 75 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
77 | | fvex 6905 |
. . . . . . . . . . . 12
β’ (((πΌ evalSub π)βπ
)βπ) β V |
78 | | fvex 6905 |
. . . . . . . . . . . 12
β’ (((πΌ evalSub π)βπ
)βπ) β V |
79 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = (((πΌ evalSub π)βπ
)βπ) β (π β π β (((πΌ evalSub π)βπ
)βπ) β π)) |
80 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
81 | | mpfind.wc |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (π β π)) |
82 | 80, 81 | elab 3669 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π₯ β£ π} β π) |
83 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = (((πΌ evalSub π)βπ
)βπ) β (π β {π₯ β£ π} β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
84 | 82, 83 | bitr3id 285 |
. . . . . . . . . . . . . . . 16
β’ (π = (((πΌ evalSub π)βπ
)βπ) β (π β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
85 | 79, 84 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (((πΌ evalSub π)βπ
)βπ) β ((π β π β§ π) β ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
86 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = (((πΌ evalSub π)βπ
)βπ) β (π β π β (((πΌ evalSub π)βπ
)βπ) β π)) |
87 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
88 | | mpfind.wd |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (π β π)) |
89 | 87, 88 | elab 3669 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π₯ β£ π} β π) |
90 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = (((πΌ evalSub π)βπ
)βπ) β (π β {π₯ β£ π} β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
91 | 89, 90 | bitr3id 285 |
. . . . . . . . . . . . . . . 16
β’ (π = (((πΌ evalSub π)βπ
)βπ) β (π β (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})) |
92 | 86, 91 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (((πΌ evalSub π)βπ
)βπ) β ((π β π β§ π) β ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) |
93 | 85, 92 | bi2anan9 638 |
. . . . . . . . . . . . . 14
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (((π β π β§ π) β§ (π β π β§ π)) β (((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) β§ ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π})))) |
94 | 93 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β (π β§ (((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) β§ ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))))) |
95 | | ovex 7442 |
. . . . . . . . . . . . . . 15
β’ (π βf + π) β V |
96 | | mpfind.we |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π βf + π) β (π β π)) |
97 | 95, 96 | elab 3669 |
. . . . . . . . . . . . . 14
β’ ((π βf + π) β {π₯ β£ π} β π) |
98 | | oveq12 7418 |
. . . . . . . . . . . . . . 15
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (π βf + π) = ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ))) |
99 | 98 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β ((π βf + π) β {π₯ β£ π} β ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π})) |
100 | 97, 99 | bitr3id 285 |
. . . . . . . . . . . . 13
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (π β ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π})) |
101 | 94, 100 | imbi12d 345 |
. . . . . . . . . . . 12
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) β ((π β§ (((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) β§ ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π}))) |
102 | | mpfind.ad |
. . . . . . . . . . . 12
β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) |
103 | 77, 78, 101, 102 | vtocl2 3552 |
. . . . . . . . . . 11
β’ ((π β§ (((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) β§ ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π}) |
104 | 64, 70, 76, 103 | syl12anc 836 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) βf + (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π}) |
105 | 63, 104 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}) |
106 | | elpreima 7060 |
. . . . . . . . . . 11
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β ((π(+gβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β ((π(+gβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}))) |
107 | 16, 106 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π(+gβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β ((π(+gβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}))) |
108 | 107 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((π(+gβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β ((π(+gβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β(π(+gβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}))) |
109 | 49, 105, 108 | mpbir2and 712 |
. . . . . . . 8
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π(+gβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
110 | 109 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π(+gβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
111 | 12, 24 | ringcl 20073 |
. . . . . . . . . 10
β’ (((πΌ mPoly (π βΎs π
)) β Ring β§ π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
)))) β (π(.rβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
112 | 35, 41, 47, 111 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π(.rβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
113 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(mulGrpβ(πΌ
mPoly (π
βΎs π
))) =
(mulGrpβ(πΌ mPoly
(π βΎs
π
))) |
114 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(mulGrpβ(π
βs (π΅ βm πΌ))) = (mulGrpβ(π βs (π΅ βm πΌ))) |
115 | 113, 114 | rhmmhm 20258 |
. . . . . . . . . . . . . 14
β’ (((πΌ evalSub π)βπ
) β ((πΌ mPoly (π βΎs π
)) RingHom (π βs (π΅ βm πΌ))) β ((πΌ evalSub π)βπ
) β ((mulGrpβ(πΌ mPoly (π βΎs π
))) MndHom (mulGrpβ(π βs (π΅ βm πΌ))))) |
116 | 5, 11, 115 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ evalSub π)βπ
) β ((mulGrpβ(πΌ mPoly (π βΎs π
))) MndHom (mulGrpβ(π βs (π΅ βm πΌ))))) |
117 | 116 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((πΌ evalSub π)βπ
) β ((mulGrpβ(πΌ mPoly (π βΎs π
))) MndHom (mulGrpβ(π βs (π΅ βm πΌ))))) |
118 | 113, 12 | mgpbas 19993 |
. . . . . . . . . . . . 13
β’
(Baseβ(πΌ mPoly
(π βΎs
π
))) =
(Baseβ(mulGrpβ(πΌ mPoly (π βΎs π
)))) |
119 | 113, 24 | mgpplusg 19991 |
. . . . . . . . . . . . 13
β’
(.rβ(πΌ mPoly (π βΎs π
))) =
(+gβ(mulGrpβ(πΌ mPoly (π βΎs π
)))) |
120 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(.rβ(π βs (π΅ βm πΌ))) =
(.rβ(π
βs (π΅ βm πΌ))) |
121 | 114, 120 | mgpplusg 19991 |
. . . . . . . . . . . . 13
β’
(.rβ(π βs (π΅ βm πΌ))) =
(+gβ(mulGrpβ(π βs (π΅ βm πΌ)))) |
122 | 118, 119,
121 | mhmlin 18679 |
. . . . . . . . . . . 12
β’ ((((πΌ evalSub π)βπ
) β ((mulGrpβ(πΌ mPoly (π βΎs π
))) MndHom (mulGrpβ(π βs (π΅ βm πΌ)))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
))) β§ π β (Baseβ(πΌ mPoly (π βΎs π
)))) β (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) = ((((πΌ evalSub π)βπ
)βπ)(.rβ(π βs (π΅ βm πΌ)))(((πΌ evalSub π)βπ
)βπ))) |
123 | 117, 41, 47, 122 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) = ((((πΌ evalSub π)βπ
)βπ)(.rβ(π βs (π΅ βm πΌ)))(((πΌ evalSub π)βπ
)βπ))) |
124 | | mpfind.ct |
. . . . . . . . . . . 12
β’ Β· =
(.rβπ) |
125 | 9, 13, 56, 57, 59, 60, 124, 120 | pwsmulrval 17437 |
. . . . . . . . . . 11
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ)(.rβ(π βs (π΅ βm πΌ)))(((πΌ evalSub π)βπ
)βπ)) = ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ))) |
126 | 123, 125 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) = ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ))) |
127 | | ovex 7442 |
. . . . . . . . . . . . . . 15
β’ (π βf Β· π) β V |
128 | | mpfind.wf |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π βf Β· π) β (π β π)) |
129 | 127, 128 | elab 3669 |
. . . . . . . . . . . . . 14
β’ ((π βf Β· π) β {π₯ β£ π} β π) |
130 | | oveq12 7418 |
. . . . . . . . . . . . . . 15
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (π βf Β· π) = ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ))) |
131 | 130 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β ((π βf Β· π) β {π₯ β£ π} β ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π})) |
132 | 129, 131 | bitr3id 285 |
. . . . . . . . . . . . 13
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (π β ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π})) |
133 | 94, 132 | imbi12d 345 |
. . . . . . . . . . . 12
β’ ((π = (((πΌ evalSub π)βπ
)βπ) β§ π = (((πΌ evalSub π)βπ
)βπ)) β (((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) β ((π β§ (((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) β§ ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π}))) |
134 | | mpfind.mu |
. . . . . . . . . . . 12
β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) |
135 | 77, 78, 133, 134 | vtocl2 3552 |
. . . . . . . . . . 11
β’ ((π β§ (((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}) β§ ((((πΌ evalSub π)βπ
)βπ) β π β§ (((πΌ evalSub π)βπ
)βπ) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π}) |
136 | 64, 70, 76, 135 | syl12anc 836 |
. . . . . . . . . 10
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((((πΌ evalSub π)βπ
)βπ) βf Β· (((πΌ evalSub π)βπ
)βπ)) β {π₯ β£ π}) |
137 | 126, 136 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}) |
138 | | elpreima 7060 |
. . . . . . . . . . 11
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β ((π(.rβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β ((π(.rβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}))) |
139 | 16, 138 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π(.rβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β ((π(.rβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}))) |
140 | 139 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β ((π(.rβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β ((π(.rβ(πΌ mPoly (π βΎs π
)))π) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β(π(.rβ(πΌ mPoly (π βΎs π
)))π)) β {π₯ β£ π}))) |
141 | 112, 137,
140 | mpbir2and 712 |
. . . . . . . 8
β’ ((π β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π(.rβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
142 | 141 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β§ (π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β§ π β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}))) β (π(.rβ(πΌ mPoly (π βΎs π
)))π) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
143 | 7 | mplassa 21581 |
. . . . . . . . . . . . 13
β’ ((πΌ β V β§ (π βΎs π
) β CRing) β (πΌ mPoly (π βΎs π
)) β AssAlg) |
144 | 26, 30, 143 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΌ mPoly (π βΎs π
)) β AssAlg) |
145 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Scalarβ(πΌ
mPoly (π
βΎs π
))) =
(Scalarβ(πΌ mPoly
(π βΎs
π
))) |
146 | 25, 145 | asclrhm 21444 |
. . . . . . . . . . . 12
β’ ((πΌ mPoly (π βΎs π
)) β AssAlg β (algScβ(πΌ mPoly (π βΎs π
))) β ((Scalarβ(πΌ mPoly (π βΎs π
))) RingHom (πΌ mPoly (π βΎs π
)))) |
147 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
)))) = (Baseβ(Scalarβ(πΌ mPoly (π βΎs π
)))) |
148 | 147, 12 | rhmf 20263 |
. . . . . . . . . . . 12
β’
((algScβ(πΌ
mPoly (π
βΎs π
)))
β ((Scalarβ(πΌ
mPoly (π
βΎs π
)))
RingHom (πΌ mPoly (π βΎs π
))) β (algScβ(πΌ mPoly (π βΎs π
))):(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))βΆ(Baseβ(πΌ mPoly (π βΎs π
)))) |
149 | 144, 146,
148 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (algScβ(πΌ mPoly (π βΎs π
))):(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))βΆ(Baseβ(πΌ mPoly (π βΎs π
)))) |
150 | 149 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (Baseβ(π βΎs π
))) β (algScβ(πΌ mPoly (π βΎs π
))):(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))βΆ(Baseβ(πΌ mPoly (π βΎs π
)))) |
151 | 7, 26, 30 | mplsca 21572 |
. . . . . . . . . . . . 13
β’ (π β (π βΎs π
) = (Scalarβ(πΌ mPoly (π βΎs π
)))) |
152 | 151 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ (π β (Baseβ(π βΎs π
)) =
(Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))) |
153 | 152 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π β (π β (Baseβ(π βΎs π
)) β π β (Baseβ(Scalarβ(πΌ mPoly (π βΎs π
)))))) |
154 | 153 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ π β (Baseβ(π βΎs π
))) β π β (Baseβ(Scalarβ(πΌ mPoly (π βΎs π
))))) |
155 | 150, 154 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ ((π β§ π β (Baseβ(π βΎs π
))) β ((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
156 | 26 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (Baseβ(π βΎs π
))) β πΌ β V) |
157 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (Baseβ(π βΎs π
))) β π β CRing) |
158 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (Baseβ(π βΎs π
))) β π
β (SubRingβπ)) |
159 | 10 | subrgss 20320 |
. . . . . . . . . . . . . 14
β’ (π
β (SubRingβπ) β π
β π΅) |
160 | 8, 10 | ressbas2 17182 |
. . . . . . . . . . . . . 14
β’ (π
β π΅ β π
= (Baseβ(π βΎs π
))) |
161 | 28, 159, 160 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β π
= (Baseβ(π βΎs π
))) |
162 | 161 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π β (π β π
β π β (Baseβ(π βΎs π
)))) |
163 | 162 | biimpar 479 |
. . . . . . . . . . 11
β’ ((π β§ π β (Baseβ(π βΎs π
))) β π β π
) |
164 | 6, 7, 8, 10, 25, 156, 157, 158, 163 | evlssca 21652 |
. . . . . . . . . 10
β’ ((π β§ π β (Baseβ(π βΎs π
))) β (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) = ((π΅ βm πΌ) Γ {π})) |
165 | | mpfind.co |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π
) β π) |
166 | 165 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ (π β βπ β π
π) |
167 | | ovex 7442 |
. . . . . . . . . . . . . . . . 17
β’ (π΅ βm πΌ) β V |
168 | | vsnex 5430 |
. . . . . . . . . . . . . . . . 17
β’ {π} β V |
169 | 167, 168 | xpex 7740 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ βm πΌ) Γ {π}) β V |
170 | | mpfind.wa |
. . . . . . . . . . . . . . . 16
β’ (π₯ = ((π΅ βm πΌ) Γ {π}) β (π β π)) |
171 | 169, 170 | elab 3669 |
. . . . . . . . . . . . . . 15
β’ (((π΅ βm πΌ) Γ {π}) β {π₯ β£ π} β π) |
172 | | sneq 4639 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β {π} = {π}) |
173 | 172 | xpeq2d 5707 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π΅ βm πΌ) Γ {π}) = ((π΅ βm πΌ) Γ {π})) |
174 | 173 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π΅ βm πΌ) Γ {π}) β {π₯ β£ π} β ((π΅ βm πΌ) Γ {π}) β {π₯ β£ π})) |
175 | 171, 174 | bitr3id 285 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β ((π΅ βm πΌ) Γ {π}) β {π₯ β£ π})) |
176 | 175 | cbvralvw 3235 |
. . . . . . . . . . . . 13
β’
(βπ β
π
π β βπ β π
((π΅ βm πΌ) Γ {π}) β {π₯ β£ π}) |
177 | 166, 176 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β βπ β π
((π΅ βm πΌ) Γ {π}) β {π₯ β£ π}) |
178 | 177 | r19.21bi 3249 |
. . . . . . . . . . 11
β’ ((π β§ π β π
) β ((π΅ βm πΌ) Γ {π}) β {π₯ β£ π}) |
179 | 163, 178 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β (Baseβ(π βΎs π
))) β ((π΅ βm πΌ) Γ {π}) β {π₯ β£ π}) |
180 | 164, 179 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π β (Baseβ(π βΎs π
))) β (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) β {π₯ β£ π}) |
181 | | elpreima 7060 |
. . . . . . . . . . 11
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β (((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) β {π₯ β£ π}))) |
182 | 16, 181 | syl 17 |
. . . . . . . . . 10
β’ (π β (((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) β {π₯ β£ π}))) |
183 | 182 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (Baseβ(π βΎs π
))) β (((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β((algScβ(πΌ mPoly (π βΎs π
)))βπ)) β {π₯ β£ π}))) |
184 | 155, 180,
183 | mpbir2and 712 |
. . . . . . . 8
β’ ((π β§ π β (Baseβ(π βΎs π
))) β ((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
185 | 184 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β§ π β (Baseβ(π βΎs π
))) β ((algScβ(πΌ mPoly (π βΎs π
)))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
186 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β πΌ β V) |
187 | 32 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (π βΎs π
) β Ring) |
188 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β π β πΌ) |
189 | 7, 22, 12, 186, 187, 188 | mvrcl 21551 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β ((πΌ mVar (π βΎs π
))βπ) β (Baseβ(πΌ mPoly (π βΎs π
)))) |
190 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β π β CRing) |
191 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β π
β (SubRingβπ)) |
192 | 6, 22, 8, 10, 186, 190, 191, 188 | evlsvar 21653 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (((πΌ evalSub π)βπ
)β((πΌ mVar (π βΎs π
))βπ)) = (π β (π΅ βm πΌ) β¦ (πβπ))) |
193 | | mpfind.pr |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΌ) β π) |
194 | 167 | mptex 7225 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ βm πΌ) β¦ (πβπ)) β V |
195 | | mpfind.wb |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π β (π΅ βm πΌ) β¦ (πβπ)) β (π β π)) |
196 | 194, 195 | elab 3669 |
. . . . . . . . . . . . . 14
β’ ((π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π} β π) |
197 | 193, 196 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π}) |
198 | 197 | ralrimiva 3147 |
. . . . . . . . . . . 12
β’ (π β βπ β πΌ (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π}) |
199 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
200 | 199 | mpteq2dv 5251 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β (π΅ βm πΌ) β¦ (πβπ)) = (π β (π΅ βm πΌ) β¦ (πβπ))) |
201 | 200 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π} β (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π})) |
202 | 201 | cbvralvw 3235 |
. . . . . . . . . . . 12
β’
(βπ β
πΌ (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π} β βπ β πΌ (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π}) |
203 | 198, 202 | sylib 217 |
. . . . . . . . . . 11
β’ (π β βπ β πΌ (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π}) |
204 | 203 | r19.21bi 3249 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (π β (π΅ βm πΌ) β¦ (πβπ)) β {π₯ β£ π}) |
205 | 192, 204 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (((πΌ evalSub π)βπ
)β((πΌ mVar (π βΎs π
))βπ)) β {π₯ β£ π}) |
206 | | elpreima 7060 |
. . . . . . . . . . 11
β’ (((πΌ evalSub π)βπ
) Fn (Baseβ(πΌ mPoly (π βΎs π
))) β (((πΌ mVar (π βΎs π
))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (((πΌ mVar (π βΎs π
))βπ) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β((πΌ mVar (π βΎs π
))βπ)) β {π₯ β£ π}))) |
207 | 16, 206 | syl 17 |
. . . . . . . . . 10
β’ (π β (((πΌ mVar (π βΎs π
))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (((πΌ mVar (π βΎs π
))βπ) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β((πΌ mVar (π βΎs π
))βπ)) β {π₯ β£ π}))) |
208 | 207 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (((πΌ mVar (π βΎs π
))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π}) β (((πΌ mVar (π βΎs π
))βπ) β (Baseβ(πΌ mPoly (π βΎs π
))) β§ (((πΌ evalSub π)βπ
)β((πΌ mVar (π βΎs π
))βπ)) β {π₯ β£ π}))) |
209 | 189, 205,
208 | mpbir2and 712 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β ((πΌ mVar (π βΎs π
))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
210 | 209 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β§ π β πΌ) β ((πΌ mVar (π βΎs π
))βπ) β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
211 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) |
212 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β πΌ β V) |
213 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β (π βΎs π
) β CRing) |
214 | 21, 22, 7, 23, 24, 25, 12, 110, 142, 185, 210, 211, 212, 213 | mplind 21631 |
. . . . . 6
β’ ((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β π¦ β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) |
215 | | fvimacnvi 7054 |
. . . . . 6
β’ ((Fun
((πΌ evalSub π)βπ
) β§ π¦ β (β‘((πΌ evalSub π)βπ
) β {π₯ β£ π})) β (((πΌ evalSub π)βπ
)βπ¦) β {π₯ β£ π}) |
216 | 20, 214, 215 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β (((πΌ evalSub π)βπ
)βπ¦) β {π₯ β£ π}) |
217 | | eleq1 2822 |
. . . . 5
β’ ((((πΌ evalSub π)βπ
)βπ¦) = π΄ β ((((πΌ evalSub π)βπ
)βπ¦) β {π₯ β£ π} β π΄ β {π₯ β£ π})) |
218 | 216, 217 | syl5ibcom 244 |
. . . 4
β’ ((π β§ π¦ β (Baseβ(πΌ mPoly (π βΎs π
)))) β ((((πΌ evalSub π)βπ
)βπ¦) = π΄ β π΄ β {π₯ β£ π})) |
219 | 218 | rexlimdva 3156 |
. . 3
β’ (π β (βπ¦ β (Baseβ(πΌ mPoly (π βΎs π
)))(((πΌ evalSub π)βπ
)βπ¦) = π΄ β π΄ β {π₯ β£ π})) |
220 | 19, 219 | mpd 15 |
. 2
β’ (π β π΄ β {π₯ β£ π}) |
221 | | mpfind.wg |
. . . 4
β’ (π₯ = π΄ β (π β π)) |
222 | 221 | elabg 3667 |
. . 3
β’ (π΄ β π β (π΄ β {π₯ β£ π} β π)) |
223 | 1, 222 | syl 17 |
. 2
β’ (π β (π΄ β {π₯ β£ π} β π)) |
224 | 220, 223 | mpbid 231 |
1
β’ (π β π) |