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\mathrm{mPwSer}R$$
	mhmcopsr.q	$$⊢Q=I\mathrm{mPwSer}S$$
	mhmcopsr.b	$$⊢B={\mathrm{Base}}_P$$
	mhmcopsr.c	$$⊢C={\mathrm{Base}}_Q$$
	mhmcopsr.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
	mhmcopsr.f	$$⊢\phi \to F\in B$$
Assertion	mhmcopsr	$$⊢\phi \to H\circ F\in C$$

Proof

Step	Hyp	Ref	Expression
1		mhmcopsr.p	$$⊢P=I\mathrm{mPwSer}R$$
2		mhmcopsr.q	$$⊢Q=I\mathrm{mPwSer}S$$
3		mhmcopsr.b	$$⊢B={\mathrm{Base}}_P$$
4		mhmcopsr.c	$$⊢C={\mathrm{Base}}_Q$$
5		mhmcopsr.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
6		mhmcopsr.f	$$⊢\phi \to F\in B$$
7		fvexd	$$⊢\phi \to {\mathrm{Base}}_S\in \mathrm{V}$$
8		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
9	8	rabex	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
13	11 12	mhmf	$$⊢H\in \left(R\mathrm{MndHom}S\right)\to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
14	5 13	syl	$$⊢\phi \to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
15		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
16	1 11 15 3 6	psrelbas	$$⊢\phi \to F:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
17	14 16	fcod	$$⊢\phi \to \left(H\circ F\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_S$$
18	7 10 17	elmapdd	$$⊢\phi \to H\circ F\in \left({{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
19		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
20	19 1 3	elbasov	$$⊢F\in B\to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
21	6 20	syl	$$⊢\phi \to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
22	21	simpld	$$⊢\phi \to I\in \mathrm{V}$$
23	2 12 15 4 22	psrbas	$$⊢\phi \to C={{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
24	18 23	eleqtrrd	$$⊢\phi \to H\circ F\in C$$