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.i 
|- ( ph -> I e. V )
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.i 
 |-  ( ph -> I e. V )
6 mhmcompl.h 
 |-  ( ph -> H e. ( R MndHom S ) )
7 mhmcompl.f 
 |-  ( ph -> F e. B )
8 fvexd 
 |-  ( ph -> ( Base ` S ) e. _V )
9 ovex 
 |-  ( NN0 ^m I ) e. _V
10 9 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
11 10 a1i 
 |-  ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( Base ` S ) = ( Base ` S )
14 12 13 mhmf 
 |-  ( H e. ( R MndHom S ) -> H : ( Base ` R ) --> ( Base ` S ) )
15 6 14 syl 
 |-  ( ph -> H : ( Base ` R ) --> ( Base ` S ) )
16 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
17 1 12 3 16 7 mplelf 
 |-  ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
18 15 17 fcod 
 |-  ( ph -> ( H o. F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` S ) )
19 8 11 18 elmapdd 
 |-  ( ph -> ( H o. F ) e. ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
20 eqid 
 |-  ( I mPwSer S ) = ( I mPwSer S )
21 eqid 
 |-  ( Base ` ( I mPwSer S ) ) = ( Base ` ( I mPwSer S ) )
22 20 13 16 21 5 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer S ) ) = ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
23 19 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 6 25 syl 
 |-  ( ph -> R e. Mnd )
27 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
28 12 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 7 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 6 34 syl 
 |-  ( ph -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) )
36 24 29 17 15 30 11 31 32 35 fsuppcor 
 |-  ( ph -> ( H o. F ) finSupp ( 0g ` S ) )
37 2 20 21 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 )