This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )