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 φ H R MndHom S
mhmcopsr.f φ F B
Assertion mhmcopsr φ H F 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 φ H R MndHom S
6 mhmcopsr.f φ F B
7 fvexd φ Base S V
8 ovex 0 I V
9 8 rabex f 0 I | f -1 Fin V
10 9 a1i φ f 0 I | f -1 Fin V
11 eqid Base R = Base R
12 eqid Base S = Base S
13 11 12 mhmf H R MndHom S H : Base R Base S
14 5 13 syl φ H : Base R Base S
15 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
16 1 11 15 3 6 psrelbas φ F : f 0 I | f -1 Fin Base R
17 14 16 fcod φ H F : f 0 I | f -1 Fin Base S
18 7 10 17 elmapdd φ H F Base S f 0 I | f -1 Fin
19 reldmpsr Rel dom mPwSer
20 19 1 3 elbasov F B I V R V
21 6 20 syl φ I V R V
22 21 simpld φ I V
23 2 12 15 4 22 psrbas φ C = Base S f 0 I | f -1 Fin
24 18 23 eleqtrrd φ H F C