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 𝑃 = ( 𝐼 mPwSer 𝑅 )
mhmcopsr.q 𝑄 = ( 𝐼 mPwSer 𝑆 )
mhmcopsr.b 𝐵 = ( Base ‘ 𝑃 )
mhmcopsr.c 𝐶 = ( Base ‘ 𝑄 )
mhmcopsr.h ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
mhmcopsr.f ( 𝜑𝐹𝐵 )
Assertion mhmcopsr ( 𝜑 → ( 𝐻𝐹 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 mhmcopsr.p 𝑃 = ( 𝐼 mPwSer 𝑅 )
2 mhmcopsr.q 𝑄 = ( 𝐼 mPwSer 𝑆 )
3 mhmcopsr.b 𝐵 = ( Base ‘ 𝑃 )
4 mhmcopsr.c 𝐶 = ( Base ‘ 𝑄 )
5 mhmcopsr.h ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
6 mhmcopsr.f ( 𝜑𝐹𝐵 )
7 fvexd ( 𝜑 → ( Base ‘ 𝑆 ) ∈ V )
8 ovex ( ℕ0m 𝐼 ) ∈ V
9 8 rabex { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V
10 9 a1i ( 𝜑 → { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V )
11 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13 11 12 mhmf ( 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
14 5 13 syl ( 𝜑𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
15 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
16 1 11 15 3 6 psrelbas ( 𝜑𝐹 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
17 14 16 fcod ( 𝜑 → ( 𝐻𝐹 ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑆 ) )
18 7 10 17 elmapdd ( 𝜑 → ( 𝐻𝐹 ) ∈ ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
19 reldmpsr Rel dom mPwSer
20 19 1 3 elbasov ( 𝐹𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
21 6 20 syl ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
22 21 simpld ( 𝜑𝐼 ∈ V )
23 2 12 15 4 22 psrbas ( 𝜑𝐶 = ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
24 18 23 eleqtrrd ( 𝜑 → ( 𝐻𝐹 ) ∈ 𝐶 )