Theorem rhmply1vsca

Description: Apply a ring homomorphism between two univariate polynomial algebras to a scaled polynomial. (Contributed by SN, 20-May-2025)

	Ref	Expression
Hypotheses	rhmply1vsca.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	rhmply1vsca.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
	rhmply1vsca.b	$$⊢B={\mathrm{Base}}_P$$
	rhmply1vsca.k	$$⊢K={\mathrm{Base}}_R$$
	rhmply1vsca.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
	rhmply1vsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	rhmply1vsca.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Q$$
	rhmply1vsca.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
	rhmply1vsca.c	$$⊢\phi \to C\in K$$
	rhmply1vsca.x	$$⊢\phi \to X\in B$$
Assertion	rhmply1vsca	$$⊢\phi \to F\left(C\underset{\dot{}}{·}X\right)=H\left(C\right)\underset{\dot{}}{\bullet }F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmply1vsca.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		rhmply1vsca.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
3		rhmply1vsca.b	$$⊢B={\mathrm{Base}}_P$$
4		rhmply1vsca.k	$$⊢K={\mathrm{Base}}_R$$
5		rhmply1vsca.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
6		rhmply1vsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
7		rhmply1vsca.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Q$$
8		rhmply1vsca.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
9		rhmply1vsca.c	$$⊢\phi \to C\in K$$
10		rhmply1vsca.x	$$⊢\phi \to X\in B$$
11		fconst6g	$$⊢C\in K\to \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right):\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
12	9 11	syl	$$⊢\phi \to \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right):\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
13		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
14	13	feq2i	$$⊢\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶K\leftrightarrow \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right):\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
15	12 14	sylibr	$$⊢\phi \to \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$
16	1 3 4	ply1basf	$$⊢X\in B\to X:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$
17	10 16	syl	$$⊢\phi \to X:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$
18		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
19	4 18	rhmf	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H:K⟶{\mathrm{Base}}_S$$
20	8 19	syl	$$⊢\phi \to H:K⟶{\mathrm{Base}}_S$$
21	20	ffnd	$$⊢\phi \to HFnK$$
22		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^{1_{𝑜}}\in \mathrm{V}$$
23		rhmrcl1	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to R\in \mathrm{Ring}$$
24	8 23	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
25		eqid	$$⊢{\cdot }_R={\cdot }_R$$
26	4 25	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge a\in K\wedge b\in K\right)\to a{\cdot }_{R}b\in K$$
27	24 26	syl3an1	$$⊢\left(\phi \wedge a\in K\wedge b\in K\right)\to a{\cdot }_{R}b\in K$$
28	27	3expb	$$⊢\left(\phi \wedge \left(a\in K\wedge b\in K\right)\right)\to a{\cdot }_{R}b\in K$$
29		eqid	$$⊢{\cdot }_S={\cdot }_S$$
30	4 25 29	rhmmul	$$⊢\left(H\in \left(R\mathrm{RingHom}S\right)\wedge a\in K\wedge b\in K\right)\to H\left(a{\cdot }_{R}b\right)=H\left(a\right){\cdot }_{S}H\left(b\right)$$
31	8 30	syl3an1	$$⊢\left(\phi \wedge a\in K\wedge b\in K\right)\to H\left(a{\cdot }_{R}b\right)=H\left(a\right){\cdot }_{S}H\left(b\right)$$
32	31	3expb	$$⊢\left(\phi \wedge \left(a\in K\wedge b\in K\right)\right)\to H\left(a{\cdot }_{R}b\right)=H\left(a\right){\cdot }_{S}H\left(b\right)$$
33	15 17 21 22 28 32	coof	$$⊢\phi \to H\circ \left(\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right){{\cdot }_R}_{f}X\right)=\left(H\circ \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right)\right){{\cdot }_S}_f\left(H\circ X\right)$$
34		fcoconst	$$⊢\left(HFnK\wedge C\in K\right)\to H\circ \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right)=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{H\left(C\right)\right\}$$
35	21 9 34	syl2anc	$$⊢\phi \to H\circ \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right)=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{H\left(C\right)\right\}$$
36	35	oveq1d	$$⊢\phi \to \left(H\circ \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right)\right){{\cdot }_S}_f\left(H\circ X\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{H\left(C\right)\right\}\right){{\cdot }_S}_f\left(H\circ X\right)$$
37	33 36	eqtrd	$$⊢\phi \to H\circ \left(\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right){{\cdot }_R}_{f}X\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{H\left(C\right)\right\}\right){{\cdot }_S}_f\left(H\circ X\right)$$
38		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
39		eqid	$$⊢{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
40	1 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
41		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
42	38 39 4 40 25 41 9 10	mplvsca	$$⊢\phi \to C{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}X=\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right){{\cdot }_R}_{f}X$$
43	42	coeq2d	$$⊢\phi \to H\circ \left(C{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}X\right)=H\circ \left(\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{C\right\}\right){{\cdot }_R}_{f}X\right)$$
44		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
45		eqid	$$⊢{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
46		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
47	2 46	ply1bas	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
48	20 9	ffvelcdmd	$$⊢\phi \to H\left(C\right)\in {\mathrm{Base}}_S$$
49		rhmghm	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H\in \left(R\mathrm{GrpHom}S\right)$$
50		ghmmhm	$$⊢H\in \left(R\mathrm{GrpHom}S\right)\to H\in \left(R\mathrm{MndHom}S\right)$$
51	8 49 50	3syl	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
52	1 2 3 46 51 10	mhmcoply1	$$⊢\phi \to H\circ X\in {\mathrm{Base}}_Q$$
53	44 45 18 47 29 41 48 52	mplvsca	$$⊢\phi \to H\left(C\right){\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}\left(H\circ X\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{H\left(C\right)\right\}\right){{\cdot }_S}_f\left(H\circ X\right)$$
54	37 43 53	3eqtr4d	$$⊢\phi \to H\circ \left(C{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}X\right)=H\left(C\right){\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}\left(H\circ X\right)$$
55	1 38 6	ply1vsca	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
56	55	oveqi	$$⊢C\underset{\dot{}}{·}X=C{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}X$$
57	56	coeq2i	$$⊢H\circ \left(C\underset{\dot{}}{·}X\right)=H\circ \left(C{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}X\right)$$
58	2 44 7	ply1vsca	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
59	58	oveqi	$$⊢H\left(C\right)\underset{\dot{}}{\bullet }\left(H\circ X\right)=H\left(C\right){\cdot }_{\left(1_{𝑜}\mathrm{mPoly}S\right)}\left(H\circ X\right)$$
60	54 57 59	3eqtr4g	$$⊢\phi \to H\circ \left(C\underset{\dot{}}{·}X\right)=H\left(C\right)\underset{\dot{}}{\bullet }\left(H\circ X\right)$$
61		coeq2	$$⊢p=C\underset{\dot{}}{·}X\to H\circ p=H\circ \left(C\underset{\dot{}}{·}X\right)$$
62	1 3 4 6 24 9 10	ply1vscl	$$⊢\phi \to C\underset{\dot{}}{·}X\in B$$
63	8 62	coexd	$$⊢\phi \to H\circ \left(C\underset{\dot{}}{·}X\right)\in \mathrm{V}$$
64	5 61 62 63	fvmptd3	$$⊢\phi \to F\left(C\underset{\dot{}}{·}X\right)=H\circ \left(C\underset{\dot{}}{·}X\right)$$
65		coeq2	$$⊢p=X\to H\circ p=H\circ X$$
66	8 10	coexd	$$⊢\phi \to H\circ X\in \mathrm{V}$$
67	5 65 10 66	fvmptd3	$$⊢\phi \to F\left(X\right)=H\circ X$$
68	67	oveq2d	$$⊢\phi \to H\left(C\right)\underset{\dot{}}{\bullet }F\left(X\right)=H\left(C\right)\underset{\dot{}}{\bullet }\left(H\circ X\right)$$
69	60 64 68	3eqtr4d	$$⊢\phi \to F\left(C\underset{\dot{}}{·}X\right)=H\left(C\right)\underset{\dot{}}{\bullet }F\left(X\right)$$