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 = ( Poly1 ` R )
	rhmply1mon.q	|- Q = ( Poly1 ` S )
	rhmply1mon.b	|- B = ( Base ` P )
	rhmply1mon.k	|- K = ( Base ` R )
	rhmply1mon.f	|- F = ( p e. B |-> ( H o. p ) )
	rhmply1mon.x	|- X = ( var1 ` R )
	rhmply1mon.y	|- Y = ( var1 ` S )
	rhmply1mon.t	|- .x. = ( .s ` P )
	rhmply1mon.u	|- .xb = ( .s ` Q )
	rhmply1mon.m	|- M = ( mulGrp ` P )
	rhmply1mon.n	|- N = ( mulGrp ` Q )
	rhmply1mon.l	|- .^ = ( .g ` M )
	rhmply1mon.w	|- ./\ = ( .g ` N )
	rhmply1mon.h	|- ( ph -> H e. ( R RingHom S ) )
	rhmply1mon.c	|- ( ph -> C e. K )
	rhmply1mon.e	|- ( ph -> E e. NN0 )
Assertion	rhmply1mon	|- ( ph -> ( F ` ( C .x. ( E .^ X ) ) ) = ( ( H ` C ) .xb ( E ./\ Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmply1mon.p	|- P = ( Poly1 ` R )
2		rhmply1mon.q	|- Q = ( Poly1 ` S )
3		rhmply1mon.b	|- B = ( Base ` P )
4		rhmply1mon.k	|- K = ( Base ` R )
5		rhmply1mon.f	|- F = ( p e. B |-> ( H o. p ) )
6		rhmply1mon.x	|- X = ( var1 ` R )
7		rhmply1mon.y	|- Y = ( var1 ` S )
8		rhmply1mon.t	|- .x. = ( .s ` P )
9		rhmply1mon.u	|- .xb = ( .s ` Q )
10		rhmply1mon.m	|- M = ( mulGrp ` P )
11		rhmply1mon.n	|- N = ( mulGrp ` Q )
12		rhmply1mon.l	|- .^ = ( .g ` M )
13		rhmply1mon.w	|- ./\ = ( .g ` N )
14		rhmply1mon.h	|- ( ph -> H e. ( R RingHom S ) )
15		rhmply1mon.c	|- ( ph -> C e. K )
16		rhmply1mon.e	|- ( ph -> E e. NN0 )
17	10 3	mgpbas	|- B = ( Base ` M )
18		rhmrcl1	|- ( H e. ( R RingHom S ) -> R e. Ring )
19	14 18	syl	|- ( ph -> R e. Ring )
20	1	ply1ring	|- ( R e. Ring -> P e. Ring )
21	19 20	syl	|- ( ph -> P e. Ring )
22	10	ringmgp	|- ( P e. Ring -> M e. Mnd )
23	21 22	syl	|- ( ph -> M e. Mnd )
24	6 1 3	vr1cl	|- ( R e. Ring -> X e. B )
25	19 24	syl	|- ( ph -> X e. B )
26	17 12 23 16 25	mulgnn0cld	|- ( ph -> ( E .^ X ) e. B )
27	1 2 3 4 5 8 9 14 15 26	rhmply1vsca	|- ( ph -> ( F ` ( C .x. ( E .^ X ) ) ) = ( ( H ` C ) .xb ( F ` ( E .^ X ) ) ) )
28	1 2 3 5 14	rhmply1	|- ( ph -> F e. ( P RingHom Q ) )
29	10 11	rhmmhm	|- ( F e. ( P RingHom Q ) -> F e. ( M MndHom N ) )
30	28 29	syl	|- ( ph -> F e. ( M MndHom N ) )
31	17 12 13	mhmmulg	|- ( ( F e. ( M MndHom N ) /\ E e. NN0 /\ X e. B ) -> ( F ` ( E .^ X ) ) = ( E ./\ ( F ` X ) ) )
32	30 16 25 31	syl3anc	|- ( ph -> ( F ` ( E .^ X ) ) = ( E ./\ ( F ` X ) ) )
33	1 2 3 5 6 7 14	rhmply1vr1	|- ( ph -> ( F ` X ) = Y )
34	33	oveq2d	|- ( ph -> ( E ./\ ( F ` X ) ) = ( E ./\ Y ) )
35	32 34	eqtrd	|- ( ph -> ( F ` ( E .^ X ) ) = ( E ./\ Y ) )
36	35	oveq2d	|- ( ph -> ( ( H ` C ) .xb ( F ` ( E .^ X ) ) ) = ( ( H ` C ) .xb ( E ./\ Y ) ) )
37	27 36	eqtrd	|- ( ph -> ( F ` ( C .x. ( E .^ X ) ) ) = ( ( H ` C ) .xb ( E ./\ Y ) ) )