Theorem rhmply1

Description: Provide a ring homomorphism between two univariate polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 20-May-2025)

	Ref	Expression
Hypotheses	rhmply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	rhmply1.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
	rhmply1.b	$$⊢B={\mathrm{Base}}_P$$
	rhmply1.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
	rhmply1.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
Assertion	rhmply1	$$⊢\phi \to F\in \left(P\mathrm{RingHom}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		rhmply1.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
3		rhmply1.b	$$⊢B={\mathrm{Base}}_P$$
4		rhmply1.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
5		rhmply1.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
8	1 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
11	6 7 8 4 10 5	rhmmpl	$$⊢\phi \to F\in \left(\left(1_{𝑜}\mathrm{mPoly}R\right)\mathrm{RingHom}\left(1_{𝑜}\mathrm{mPoly}S\right)\right)$$
12	3	a1i	$$⊢\phi \to B={\mathrm{Base}}_P$$
13		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
14	13	a1i	$$⊢\phi \to {\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
15	8	a1i	$$⊢\phi \to B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
16	2 13	ply1bas	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
17	16	a1i	$$⊢\phi \to {\mathrm{Base}}_Q={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
18		eqid	$$⊢{+}_P={+}_P$$
19	1 6 18	ply1plusg	$$⊢{+}_P={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20	19	oveqi	$$⊢x{+}_{P}y=x{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
21	20	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{P}y=x{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
22		eqid	$$⊢{+}_Q={+}_Q$$
23	2 7 22	ply1plusg	$$⊢{+}_Q={+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
24	23	oveqi	$$⊢x{+}_{Q}y=x{+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}y$$
25	24	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_Q\wedge y\in {\mathrm{Base}}_Q\right)\right)\to x{+}_{Q}y=x{+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}y$$
26		eqid	$$⊢{\cdot }_P={\cdot }_P$$
27	1 6 26	ply1mulr	$$⊢{\cdot }_P={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
28	27	oveqi	$$⊢x{\cdot }_{P}y=x{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
29	28	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{P}y=x{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
30		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
31	2 7 30	ply1mulr	$$⊢{\cdot }_Q={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
32	31	oveqi	$$⊢x{\cdot }_{Q}y=x{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}y$$
33	32	a1i	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_Q\wedge y\in {\mathrm{Base}}_Q\right)\right)\to x{\cdot }_{Q}y=x{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}y$$
34	12 14 15 17 21 25 29 33	rhmpropd	$$⊢\phi \to P\mathrm{RingHom}Q=\left(1_{𝑜}\mathrm{mPoly}R\right)\mathrm{RingHom}\left(1_{𝑜}\mathrm{mPoly}S\right)$$
35	11 34	eleqtrrd	$$⊢\phi \to F\in \left(P\mathrm{RingHom}Q\right)$$