Description: The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 20-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mhmcoply1.p | |- P = ( Poly1 ` R ) |
|
mhmcoply1.q | |- Q = ( Poly1 ` S ) |
||
mhmcoply1.b | |- B = ( Base ` P ) |
||
mhmcoply1.c | |- C = ( Base ` Q ) |
||
mhmcoply1.h | |- ( ph -> H e. ( R MndHom S ) ) |
||
mhmcoply1.f | |- ( ph -> F e. B ) |
||
Assertion | mhmcoply1 | |- ( ph -> ( H o. F ) e. C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhmcoply1.p | |- P = ( Poly1 ` R ) |
|
2 | mhmcoply1.q | |- Q = ( Poly1 ` S ) |
|
3 | mhmcoply1.b | |- B = ( Base ` P ) |
|
4 | mhmcoply1.c | |- C = ( Base ` Q ) |
|
5 | mhmcoply1.h | |- ( ph -> H e. ( R MndHom S ) ) |
|
6 | mhmcoply1.f | |- ( ph -> F e. B ) |
|
7 | eqid | |- ( 1o mPoly R ) = ( 1o mPoly R ) |
|
8 | eqid | |- ( 1o mPoly S ) = ( 1o mPoly S ) |
|
9 | 1 3 | ply1bas | |- B = ( Base ` ( 1o mPoly R ) ) |
10 | 2 4 | ply1bas | |- C = ( Base ` ( 1o mPoly S ) ) |
11 | 7 8 9 10 5 6 | mhmcompl | |- ( ph -> ( H o. F ) e. C ) |