Metamath Proof Explorer


Theorem mhmcompl

Description: The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025)

Ref Expression
Hypotheses mhmcompl.p
|- P = ( I mPoly R )
mhmcompl.q
|- Q = ( I mPoly S )
mhmcompl.b
|- B = ( Base ` P )
mhmcompl.c
|- C = ( Base ` Q )
mhmcompl.h
|- ( ph -> H e. ( R MndHom S ) )
mhmcompl.f
|- ( ph -> F e. B )
Assertion mhmcompl
|- ( ph -> ( H o. F ) e. C )

Proof

Step Hyp Ref Expression
1 mhmcompl.p
 |-  P = ( I mPoly R )
2 mhmcompl.q
 |-  Q = ( I mPoly S )
3 mhmcompl.b
 |-  B = ( Base ` P )
4 mhmcompl.c
 |-  C = ( Base ` Q )
5 mhmcompl.h
 |-  ( ph -> H e. ( R MndHom S ) )
6 mhmcompl.f
 |-  ( ph -> F e. B )
7 fvexd
 |-  ( ph -> ( Base ` S ) e. _V )
8 eqid
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
9 ovexd
 |-  ( ph -> ( NN0 ^m I ) e. _V )
10 8 9 rabexd
 |-  ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
11 eqid
 |-  ( Base ` R ) = ( Base ` R )
12 eqid
 |-  ( Base ` S ) = ( Base ` S )
13 11 12 mhmf
 |-  ( H e. ( R MndHom S ) -> H : ( Base ` R ) --> ( Base ` S ) )
14 5 13 syl
 |-  ( ph -> H : ( Base ` R ) --> ( Base ` S ) )
15 1 11 3 8 6 mplelf
 |-  ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
16 14 15 fcod
 |-  ( ph -> ( H o. F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` S ) )
17 7 10 16 elmapdd
 |-  ( ph -> ( H o. F ) e. ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
18 eqid
 |-  ( I mPwSer S ) = ( I mPwSer S )
19 eqid
 |-  ( Base ` ( I mPwSer S ) ) = ( Base ` ( I mPwSer S ) )
20 1 3 mplrcl
 |-  ( F e. B -> I e. _V )
21 6 20 syl
 |-  ( ph -> I e. _V )
22 18 12 8 19 21 psrbas
 |-  ( ph -> ( Base ` ( I mPwSer S ) ) = ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
23 17 22 eleqtrrd
 |-  ( ph -> ( H o. F ) e. ( Base ` ( I mPwSer S ) ) )
24 fvexd
 |-  ( ph -> ( 0g ` S ) e. _V )
25 mhmrcl1
 |-  ( H e. ( R MndHom S ) -> R e. Mnd )
26 5 25 syl
 |-  ( ph -> R e. Mnd )
27 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
28 11 27 mndidcl
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
29 26 28 syl
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
30 ssidd
 |-  ( ph -> ( Base ` R ) C_ ( Base ` R ) )
31 fvexd
 |-  ( ph -> ( Base ` R ) e. _V )
32 1 3 27 6 26 mplelsfi
 |-  ( ph -> F finSupp ( 0g ` R ) )
33 eqid
 |-  ( 0g ` S ) = ( 0g ` S )
34 27 33 mhm0
 |-  ( H e. ( R MndHom S ) -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) )
35 5 34 syl
 |-  ( ph -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) )
36 24 29 15 14 30 10 31 32 35 fsuppcor
 |-  ( ph -> ( H o. F ) finSupp ( 0g ` S ) )
37 2 18 19 33 4 mplelbas
 |-  ( ( H o. F ) e. C <-> ( ( H o. F ) e. ( Base ` ( I mPwSer S ) ) /\ ( H o. F ) finSupp ( 0g ` S ) ) )
38 23 36 37 sylanbrc
 |-  ( ph -> ( H o. F ) e. C )