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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	rhmply1.q	⊢ 𝑄 = ( Poly1 ‘ 𝑆 )
	rhmply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	rhmply1.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
	rhmply1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion	rhmply1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		rhmply1.q	⊢ 𝑄 = ( Poly1 ‘ 𝑆 )
3		rhmply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		rhmply1.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
5		rhmply1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
6		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
7		eqid	⊢ ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
8	1 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
9		1oex	⊢ 1o ∈ V
10	9	a1i	⊢ ( 𝜑 → 1o ∈ V )
11	6 7 8 4 10 5	rhmmpl	⊢ ( 𝜑 → 𝐹 ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 1o mPoly 𝑆 ) ) )
12	3	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
13		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
14	13	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) )
15	8	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
16	2 13	ply1bas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
17	16	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑆 ) ) )
18		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
19	1 6 18	ply1plusg	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
20	19	oveqi	⊢ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑅 ) ) 𝑦 )
21	20	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
22		eqid	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
23	2 7 22	ply1plusg	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ ( 1o mPoly 𝑆 ) )
24	23	oveqi	⊢ ( 𝑥 ( +g ‘ 𝑄 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑆 ) ) 𝑦 )
25	24	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝑥 ( +g ‘ 𝑄 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑆 ) ) 𝑦 ) )
26		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
27	1 6 26	ply1mulr	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ ( 1o mPoly 𝑅 ) )
28	27	oveqi	⊢ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑅 ) ) 𝑦 )
29	28	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
30		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
31	2 7 30	ply1mulr	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ ( 1o mPoly 𝑆 ) )
32	31	oveqi	⊢ ( 𝑥 ( .r ‘ 𝑄 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑆 ) ) 𝑦 )
33	32	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝑥 ( .r ‘ 𝑄 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑆 ) ) 𝑦 ) )
34	12 14 15 17 21 25 29 33	rhmpropd	⊢ ( 𝜑 → ( 𝑃 RingHom 𝑄 ) = ( ( 1o mPoly 𝑅 ) RingHom ( 1o mPoly 𝑆 ) ) )
35	11 34	eleqtrrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )