Theorem rhmply1mon

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

	Ref	Expression
Hypotheses	rhmply1mon.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	rhmply1mon.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
	rhmply1mon.b	$$⊢B={\mathrm{Base}}_P$$
	rhmply1mon.k	$$⊢K={\mathrm{Base}}_R$$
	rhmply1mon.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
	rhmply1mon.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	rhmply1mon.y	$$⊢Y={\mathrm{var}}_1\left(S\right)$$
	rhmply1mon.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	rhmply1mon.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Q$$
	rhmply1mon.m	$$⊢M={\mathrm{mulGrp}}_P$$
	rhmply1mon.n	$$⊢N={\mathrm{mulGrp}}_Q$$
	rhmply1mon.l	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	rhmply1mon.w	$$⊢\underset{\dot{}}{\wedge }={\cdot }_N$$
	rhmply1mon.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
	rhmply1mon.c	$$⊢\phi \to C\in K$$
	rhmply1mon.e	$$⊢\phi \to E\in {\mathbb{N}}_0$$
Assertion	rhmply1mon	$$⊢\phi \to F\left(C\underset{\dot{}}{·}\left(E\underset{\dot{}}{\times }X\right)\right)=H\left(C\right)\underset{\dot{}}{\bullet }\left(E\underset{\dot{}}{\wedge }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmply1mon.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		rhmply1mon.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
3		rhmply1mon.b	$$⊢B={\mathrm{Base}}_P$$
4		rhmply1mon.k	$$⊢K={\mathrm{Base}}_R$$
5		rhmply1mon.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
6		rhmply1mon.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
7		rhmply1mon.y	$$⊢Y={\mathrm{var}}_1\left(S\right)$$
8		rhmply1mon.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
9		rhmply1mon.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Q$$
10		rhmply1mon.m	$$⊢M={\mathrm{mulGrp}}_P$$
11		rhmply1mon.n	$$⊢N={\mathrm{mulGrp}}_Q$$
12		rhmply1mon.l	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
13		rhmply1mon.w	$$⊢\underset{\dot{}}{\wedge }={\cdot }_N$$
14		rhmply1mon.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
15		rhmply1mon.c	$$⊢\phi \to C\in K$$
16		rhmply1mon.e	$$⊢\phi \to E\in {\mathbb{N}}_0$$
17	10 3	mgpbas	$$⊢B={\mathrm{Base}}_M$$
18		rhmrcl1	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to R\in \mathrm{Ring}$$
19	14 18	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
20	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
21	19 20	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
22	10	ringmgp	$$⊢P\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
23	21 22	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
24	6 1 3	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
25	19 24	syl	$$⊢\phi \to X\in B$$
26	17 12 23 16 25	mulgnn0cld	$$⊢\phi \to E\underset{\dot{}}{\times }X\in B$$
27	1 2 3 4 5 8 9 14 15 26	rhmply1vsca	$$⊢\phi \to F\left(C\underset{\dot{}}{·}\left(E\underset{\dot{}}{\times }X\right)\right)=H\left(C\right)\underset{\dot{}}{\bullet }F\left(E\underset{\dot{}}{\times }X\right)$$
28	1 2 3 5 14	rhmply1	$$⊢\phi \to F\in \left(P\mathrm{RingHom}Q\right)$$
29	10 11	rhmmhm	$$⊢F\in \left(P\mathrm{RingHom}Q\right)\to F\in \left(M\mathrm{MndHom}N\right)$$
30	28 29	syl	$$⊢\phi \to F\in \left(M\mathrm{MndHom}N\right)$$
31	17 12 13	mhmmulg	$$⊢\left(F\in \left(M\mathrm{MndHom}N\right)\wedge E\in {\mathbb{N}}_0\wedge X\in B\right)\to F\left(E\underset{\dot{}}{\times }X\right)=E\underset{\dot{}}{\wedge }F\left(X\right)$$
32	30 16 25 31	syl3anc	$$⊢\phi \to F\left(E\underset{\dot{}}{\times }X\right)=E\underset{\dot{}}{\wedge }F\left(X\right)$$
33	1 2 3 5 6 7 14	rhmply1vr1	$$⊢\phi \to F\left(X\right)=Y$$
34	33	oveq2d	$$⊢\phi \to E\underset{\dot{}}{\wedge }F\left(X\right)=E\underset{\dot{}}{\wedge }Y$$
35	32 34	eqtrd	$$⊢\phi \to F\left(E\underset{\dot{}}{\times }X\right)=E\underset{\dot{}}{\wedge }Y$$
36	35	oveq2d	$$⊢\phi \to H\left(C\right)\underset{\dot{}}{\bullet }F\left(E\underset{\dot{}}{\times }X\right)=H\left(C\right)\underset{\dot{}}{\bullet }\left(E\underset{\dot{}}{\wedge }Y\right)$$
37	27 36	eqtrd	$$⊢\phi \to F\left(C\underset{\dot{}}{·}\left(E\underset{\dot{}}{\times }X\right)\right)=H\left(C\right)\underset{\dot{}}{\bullet }\left(E\underset{\dot{}}{\wedge }Y\right)$$