Theorem evl1maprhm

Description: The function F mapping polynomials p to their evaluation at a given point X is a ring homomorphism. (Contributed by metakunt, 19-May-2025)

	Ref	Expression
Hypotheses	evl1maprhm.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1maprhm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	evl1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evl1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evl1maprhm.y	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	evl1maprhm.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
Assertion	evl1maprhm	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		evl1maprhm.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1maprhm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		evl1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evl1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
5		evl1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		evl1maprhm.y	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		evl1maprhm.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
8	7	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ) )
9		ssidd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
10	5	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
11	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13	12	subrgid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
14	11 13	syl	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
15	14	elexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
16		eqid	⊢ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = ( 𝑅 ↾s ( Base ‘ 𝑅 ) )
17	16 12	ressid2	⊢ ( ( ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) ∧ 𝑅 ∈ V ∧ ( Base ‘ 𝑅 ) ∈ V ) → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
18	9 10 15 17	syl3anc	⊢ ( 𝜑 → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
19		eqcom	⊢ ( ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 ↔ 𝑅 = ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
20	19	imbi2i	⊢ ( ( 𝜑 → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 ) ↔ ( 𝜑 → 𝑅 = ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) )
21	18 20	mpbi	⊢ ( 𝜑 → 𝑅 = ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
22	21	fveq2d	⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) )
23	2 22	eqtrid	⊢ ( 𝜑 → 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) )
24	23	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) )
25	4 24	eqtrid	⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) )
26	1 12	evl1fval1	⊢ 𝑂 = ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) )
27	26	a1i	⊢ ( 𝜑 → 𝑂 = ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) )
28	27	fveq1d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑝 ) = ( ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) ‘ 𝑝 ) )
29	28	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) ‘ 𝑝 ) ‘ 𝑋 ) )
30	25 29	mpteq12dv	⊢ ( 𝜑 → ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ) = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) ↦ ( ( ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) ‘ 𝑝 ) ‘ 𝑋 ) ) )
31		eqid	⊢ ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) = ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) )
32		eqid	⊢ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) = ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
33		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) )
34	6 3	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
35		eqid	⊢ ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) ↦ ( ( ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) ‘ 𝑝 ) ‘ 𝑋 ) ) = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) ↦ ( ( ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) ‘ 𝑝 ) ‘ 𝑋 ) )
36	31 32 12 33 5 14 34 35	evls1maprhm	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) ↦ ( ( ( 𝑅 evalSub1 ( Base ‘ 𝑅 ) ) ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) RingHom 𝑅 ) )
37	30 36	eqeltrd	⊢ ( 𝜑 → ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) RingHom 𝑅 ) )
38	2	a1i	⊢ ( 𝜑 → 𝑃 = ( Poly1 ‘ 𝑅 ) )
39	18	eqcomd	⊢ ( 𝜑 → 𝑅 = ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
40	39	fveq2d	⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) )
41	38 40	eqtr2d	⊢ ( 𝜑 → ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) = 𝑃 )
42	41	oveq1d	⊢ ( 𝜑 → ( ( Poly1 ‘ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) RingHom 𝑅 ) = ( 𝑃 RingHom 𝑅 ) )
43	37 42	eleqtrd	⊢ ( 𝜑 → ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( 𝑃 RingHom 𝑅 ) )
44	8 43	eqeltrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )