Theorem 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={\mathrm{PwSer}}_1\left(R\right)$$
	rhmpsr1.q	$$⊢Q={\mathrm{PwSer}}_1\left(S\right)$$
	rhmpsr1.b	$$⊢B={\mathrm{Base}}_P$$
	rhmpsr1.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
	rhmpsr1.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
Assertion	rhmpsr1	$$⊢\phi \to F\in \left(P\mathrm{RingHom}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmpsr1.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
2		rhmpsr1.q	$$⊢Q={\mathrm{PwSer}}_1\left(S\right)$$
3		rhmpsr1.b	$$⊢B={\mathrm{Base}}_P$$
4		rhmpsr1.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
5		rhmpsr1.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}S=1_{𝑜}\mathrm{mPwSer}S$$
8	1 3 6	psr1bas2	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
9		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
11	6 7 8 4 10 5	rhmpsr	$$⊢\phi \to F\in \left(\left(1_{𝑜}\mathrm{mPwSer}R\right)\mathrm{RingHom}\left(1_{𝑜}\mathrm{mPwSer}S\right)\right)$$
12		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
13	1 12 6	psr1bas2	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
14	13	a1i	$$⊢\phi \to {\mathrm{Base}}_P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
15		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
16	2 15 7	psr1bas2	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
17	16	a1i	$$⊢\phi \to {\mathrm{Base}}_Q={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
18		eqidd	$$⊢\phi \to {\mathrm{Base}}_P={\mathrm{Base}}_P$$
19		eqidd	$$⊢\phi \to {\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
20		eqid	$$⊢{+}_P={+}_P$$
21	1 6 20	psr1plusg	$$⊢{+}_P={+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
22	21	eqcomi	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={+}_P$$
23	22	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_P\wedge y\in {\mathrm{Base}}_P\right)\right)\to {+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={+}_P$$
24	23	oveqd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_P\wedge y\in {\mathrm{Base}}_P\right)\right)\to x{+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}y=x{+}_{P}y$$
25		eqid	$$⊢{+}_Q={+}_Q$$
26	2 7 25	psr1plusg	$$⊢{+}_Q={+}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
27	26	eqcomi	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}={+}_Q$$
28	27	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_Q\wedge y\in {\mathrm{Base}}_Q\right)\right)\to {+}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}={+}_Q$$
29	28	oveqd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_Q\wedge y\in {\mathrm{Base}}_Q\right)\right)\to x{+}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}y=x{+}_{Q}y$$
30		eqid	$$⊢{\cdot }_P={\cdot }_P$$
31	1 6 30	psr1mulr	$$⊢{\cdot }_P={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
32	31	eqcomi	$$⊢{\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\cdot }_P$$
33	32	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_P\wedge y\in {\mathrm{Base}}_P\right)\right)\to {\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\cdot }_P$$
34	33	oveqd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_P\wedge y\in {\mathrm{Base}}_P\right)\right)\to x{\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}y=x{\cdot }_{P}y$$
35		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
36	2 7 35	psr1mulr	$$⊢{\cdot }_Q={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
37	36	eqcomi	$$⊢{\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}={\cdot }_Q$$
38	37	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_Q\wedge y\in {\mathrm{Base}}_Q\right)\right)\to {\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}={\cdot }_Q$$
39	38	oveqd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_Q\wedge y\in {\mathrm{Base}}_Q\right)\right)\to x{\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}y=x{\cdot }_{Q}y$$
40	14 17 18 19 24 29 34 39	rhmpropd	$$⊢\phi \to \left(1_{𝑜}\mathrm{mPwSer}R\right)\mathrm{RingHom}\left(1_{𝑜}\mathrm{mPwSer}S\right)=P\mathrm{RingHom}Q$$
41	11 40	eleqtrd	$$⊢\phi \to F\in \left(P\mathrm{RingHom}Q\right)$$