Metamath Proof Explorer


Theorem mhmcopsr

Description: The composition of a monoid homomorphism and a power series is a power series. (Contributed by SN, 18-May-2025)

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

Proof

Step Hyp Ref Expression
1 mhmcopsr.p
 |-  P = ( I mPwSer R )
2 mhmcopsr.q
 |-  Q = ( I mPwSer S )
3 mhmcopsr.b
 |-  B = ( Base ` P )
4 mhmcopsr.c
 |-  C = ( Base ` Q )
5 mhmcopsr.h
 |-  ( ph -> H e. ( R MndHom S ) )
6 mhmcopsr.f
 |-  ( ph -> F e. B )
7 fvexd
 |-  ( ph -> ( Base ` S ) e. _V )
8 ovex
 |-  ( NN0 ^m I ) e. _V
9 8 rabex
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
10 9 a1i
 |-  ( 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 eqid
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
16 1 11 15 3 6 psrelbas
 |-  ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
17 14 16 fcod
 |-  ( ph -> ( H o. F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` S ) )
18 7 10 17 elmapdd
 |-  ( ph -> ( H o. F ) e. ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
19 reldmpsr
 |-  Rel dom mPwSer
20 19 1 3 elbasov
 |-  ( F e. B -> ( I e. _V /\ R e. _V ) )
21 6 20 syl
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
22 21 simpld
 |-  ( ph -> I e. _V )
23 2 12 15 4 22 psrbas
 |-  ( ph -> C = ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
24 18 23 eleqtrrd
 |-  ( ph -> ( H o. F ) e. C )