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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	rhmply1vsca.q	⊢ 𝑄 = ( Poly1 ‘ 𝑆 )
	rhmply1vsca.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	rhmply1vsca.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	rhmply1vsca.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
	rhmply1vsca.t	⊢ · = ( ·𝑠 ‘ 𝑃 )
	rhmply1vsca.u	⊢ ∙ = ( ·𝑠 ‘ 𝑄 )
	rhmply1vsca.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
	rhmply1vsca.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	rhmply1vsca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	rhmply1vsca	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmply1vsca.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		rhmply1vsca.q	⊢ 𝑄 = ( Poly1 ‘ 𝑆 )
3		rhmply1vsca.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		rhmply1vsca.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		rhmply1vsca.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
6		rhmply1vsca.t	⊢ · = ( ·𝑠 ‘ 𝑃 )
7		rhmply1vsca.u	⊢ ∙ = ( ·𝑠 ‘ 𝑄 )
8		rhmply1vsca.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
9		rhmply1vsca.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
10		rhmply1vsca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11		fconst6g	⊢ ( 𝐶 ∈ 𝐾 → ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
12	9 11	syl	⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
13		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
14	13	feq2i	⊢ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ↔ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
15	12 14	sylibr	⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
16	1 3 4	ply1basf	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
17	10 16	syl	⊢ ( 𝜑 → 𝑋 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
18		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
19	4 18	rhmf	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
20	8 19	syl	⊢ ( 𝜑 → 𝐻 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
21	20	ffnd	⊢ ( 𝜑 → 𝐻 Fn 𝐾 )
22		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 1o ) ∈ V )
23		rhmrcl1	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
24	8 23	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
25		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26	4 25	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝐾 )
27	24 26	syl3an1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝐾 )
28	27	3expb	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝐾 )
29		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
30	4 25 29	rhmmul	⊢ ( ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝐻 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
31	8 30	syl3an1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝐻 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
32	31	3expb	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) ) → ( 𝐻 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) )
33	15 17 21 22 28 32	coof	⊢ ( 𝜑 → ( 𝐻 ∘ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) ) = ( ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) )
34		fcoconst	⊢ ( ( 𝐻 Fn 𝐾 ∧ 𝐶 ∈ 𝐾 ) → ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) = ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) )
35	21 9 34	syl2anc	⊢ ( 𝜑 → ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) = ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) )
36	35	oveq1d	⊢ ( 𝜑 → ( ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) )
37	33 36	eqtrd	⊢ ( 𝜑 → ( 𝐻 ∘ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) )
38		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
39		eqid	⊢ ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
40	1 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
41		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
42	38 39 4 40 25 41 9 10	mplvsca	⊢ ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) )
43	42	coeq2d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) ) = ( 𝐻 ∘ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) ) )
44		eqid	⊢ ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
45		eqid	⊢ ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) = ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) )
46		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
47	2 46	ply1bas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
48	20 9	ffvelcdmd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐶 ) ∈ ( Base ‘ 𝑆 ) )
49		rhmghm	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
50		ghmmhm	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
51	8 49 50	3syl	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
52	1 2 3 46 51 10	mhmcoply1	⊢ ( 𝜑 → ( 𝐻 ∘ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
53	44 45 18 47 29 41 48 52	mplvsca	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐶 ) ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) ( 𝐻 ∘ 𝑋 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) )
54	37 43 53	3eqtr4d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) ( 𝐻 ∘ 𝑋 ) ) )
55	1 38 6	ply1vsca	⊢ · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
56	55	oveqi	⊢ ( 𝐶 · 𝑋 ) = ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 )
57	56	coeq2i	⊢ ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) = ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) )
58	2 44 7	ply1vsca	⊢ ∙ = ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) )
59	58	oveqi	⊢ ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐻 ∘ 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) ( 𝐻 ∘ 𝑋 ) )
60	54 57 59	3eqtr4g	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐻 ∘ 𝑋 ) ) )
61		coeq2	⊢ ( 𝑝 = ( 𝐶 · 𝑋 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) )
62	1 3 4 6 24 9 10	ply1vscl	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ 𝐵 )
63	8 62	coexd	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) ∈ V )
64	5 61 62 63	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) )
65		coeq2	⊢ ( 𝑝 = 𝑋 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑋 ) )
66	8 10	coexd	⊢ ( 𝜑 → ( 𝐻 ∘ 𝑋 ) ∈ V )
67	5 65 10 66	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( 𝐻 ∘ 𝑋 ) )
68	67	oveq2d	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐻 ∘ 𝑋 ) ) )
69	60 64 68	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐹 ‘ 𝑋 ) ) )