rhmpsr1

Description: Provide a ring homomorphism between two univariate power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025)

	Ref	Expression
Hypotheses	rhmpsr1.p	\|- P = ( PwSer1 ` R )
	rhmpsr1.q	\|- Q = ( PwSer1 ` S )
	rhmpsr1.b	\|- B = ( Base ` P )
	rhmpsr1.f	\|- F = ( p e. B \|-> ( H o. p ) )
	rhmpsr1.h	\|- ( ph -> H e. ( R RingHom S ) )
Assertion	rhmpsr1	\|- ( ph -> F e. ( P RingHom Q ) )

Proof

Step	Hyp	Ref	Expression
1		rhmpsr1.p	\|- P = ( PwSer1 ` R )
2		rhmpsr1.q	\|- Q = ( PwSer1 ` S )
3		rhmpsr1.b	\|- B = ( Base ` P )
4		rhmpsr1.f	\|- F = ( p e. B \|-> ( H o. p ) )
5		rhmpsr1.h	\|- ( ph -> H e. ( R RingHom S ) )
6		eqid	\|- ( 1o mPwSer R ) = ( 1o mPwSer R )
7		eqid	\|- ( 1o mPwSer S ) = ( 1o mPwSer S )
8	1 3 6	psr1bas2	\|- B = ( Base ` ( 1o mPwSer R ) )
9		1oex	\|- 1o e. _V
10	9	a1i	\|- ( ph -> 1o e. _V )
11	6 7 8 4 10 5	rhmpsr	\|- ( ph -> F e. ( ( 1o mPwSer R ) RingHom ( 1o mPwSer S ) ) )
12		eqid	\|- ( Base ` P ) = ( Base ` P )
13	1 12 6	psr1bas2	\|- ( Base ` P ) = ( Base ` ( 1o mPwSer R ) )
14	13	a1i	\|- ( ph -> ( Base ` P ) = ( Base ` ( 1o mPwSer R ) ) )
15		eqid	\|- ( Base ` Q ) = ( Base ` Q )
16	2 15 7	psr1bas2	\|- ( Base ` Q ) = ( Base ` ( 1o mPwSer S ) )
17	16	a1i	\|- ( ph -> ( Base ` Q ) = ( Base ` ( 1o mPwSer S ) ) )
18		eqidd	\|- ( ph -> ( Base ` P ) = ( Base ` P ) )
19		eqidd	\|- ( ph -> ( Base ` Q ) = ( Base ` Q ) )
20		eqid	\|- ( +g ` P ) = ( +g ` P )
21	1 6 20	psr1plusg	\|- ( +g ` P ) = ( +g ` ( 1o mPwSer R ) )
22	21	eqcomi	\|- ( +g ` ( 1o mPwSer R ) ) = ( +g ` P )
23	22	a1i	\|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( +g ` ( 1o mPwSer R ) ) = ( +g ` P ) )
24	23	oveqd	\|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( +g ` ( 1o mPwSer R ) ) y ) = ( x ( +g ` P ) y ) )
25		eqid	\|- ( +g ` Q ) = ( +g ` Q )
26	2 7 25	psr1plusg	\|- ( +g ` Q ) = ( +g ` ( 1o mPwSer S ) )
27	26	eqcomi	\|- ( +g ` ( 1o mPwSer S ) ) = ( +g ` Q )
28	27	a1i	\|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( +g ` ( 1o mPwSer S ) ) = ( +g ` Q ) )
29	28	oveqd	\|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( +g ` ( 1o mPwSer S ) ) y ) = ( x ( +g ` Q ) y ) )
30		eqid	\|- ( .r ` P ) = ( .r ` P )
31	1 6 30	psr1mulr	\|- ( .r ` P ) = ( .r ` ( 1o mPwSer R ) )
32	31	eqcomi	\|- ( .r ` ( 1o mPwSer R ) ) = ( .r ` P )
33	32	a1i	\|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( .r ` ( 1o mPwSer R ) ) = ( .r ` P ) )
34	33	oveqd	\|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` ( 1o mPwSer R ) ) y ) = ( x ( .r ` P ) y ) )
35		eqid	\|- ( .r ` Q ) = ( .r ` Q )
36	2 7 35	psr1mulr	\|- ( .r ` Q ) = ( .r ` ( 1o mPwSer S ) )
37	36	eqcomi	\|- ( .r ` ( 1o mPwSer S ) ) = ( .r ` Q )
38	37	a1i	\|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( .r ` ( 1o mPwSer S ) ) = ( .r ` Q ) )
39	38	oveqd	\|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( .r ` ( 1o mPwSer S ) ) y ) = ( x ( .r ` Q ) y ) )
40	14 17 18 19 24 29 34 39	rhmpropd	\|- ( ph -> ( ( 1o mPwSer R ) RingHom ( 1o mPwSer S ) ) = ( P RingHom Q ) )
41	11 40	eleqtrd	\|- ( ph -> F e. ( P RingHom Q ) )

Metamath Proof Explorer

Theorem rhmpsr1

Proof