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 𝑃 = ( Poly1𝑅 )
mhmcoply1.q 𝑄 = ( Poly1𝑆 )
mhmcoply1.b 𝐵 = ( Base ‘ 𝑃 )
mhmcoply1.c 𝐶 = ( Base ‘ 𝑄 )
mhmcoply1.h ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
mhmcoply1.f ( 𝜑𝐹𝐵 )
Assertion mhmcoply1 ( 𝜑 → ( 𝐻𝐹 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 mhmcoply1.p 𝑃 = ( Poly1𝑅 )
2 mhmcoply1.q 𝑄 = ( Poly1𝑆 )
3 mhmcoply1.b 𝐵 = ( Base ‘ 𝑃 )
4 mhmcoply1.c 𝐶 = ( Base ‘ 𝑄 )
5 mhmcoply1.h ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
6 mhmcoply1.f ( 𝜑𝐹𝐵 )
7 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8 eqid ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
9 1 3 ply1bas 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
10 2 4 ply1bas 𝐶 = ( Base ‘ ( 1o mPoly 𝑆 ) )
11 7 8 9 10 5 6 mhmcompl ( 𝜑 → ( 𝐻𝐹 ) ∈ 𝐶 )