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 )