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 | ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 ) |
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 | ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 ) |