Metamath Proof Explorer


Theorem mhmcoply1

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 )

Proof

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 )