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	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	evl1maprhm.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	evl1maprhm.b	$$⊢B={\mathrm{Base}}_R$$
	evl1maprhm.u	$$⊢U={\mathrm{Base}}_P$$
	evl1maprhm.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1maprhm.y	$$⊢\phi \to X\in B$$
	evl1maprhm.f	$$⊢F=\left(p\in U⟼O\left(p\right)\left(X\right)\right)$$
Assertion	evl1maprhm	$$⊢\phi \to F\in \left(P\mathrm{RingHom}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1maprhm.q	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		evl1maprhm.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		evl1maprhm.b	$$⊢B={\mathrm{Base}}_R$$
4		evl1maprhm.u	$$⊢U={\mathrm{Base}}_P$$
5		evl1maprhm.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		evl1maprhm.y	$$⊢\phi \to X\in B$$
7		evl1maprhm.f	$$⊢F=\left(p\in U⟼O\left(p\right)\left(X\right)\right)$$
8	7	a1i	$$⊢\phi \to F=\left(p\in U⟼O\left(p\right)\left(X\right)\right)$$
9		ssidd	$$⊢\phi \to {\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R$$
10	5	elexd	$$⊢\phi \to R\in \mathrm{V}$$
11	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13	12	subrgid	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_R\in \mathrm{SubRing}\left(R\right)$$
14	11 13	syl	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{SubRing}\left(R\right)$$
15	14	elexd	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{V}$$
16		eqid	$$⊢R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R$$
17	16 12	ressid2	$$⊢\left({\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R\wedge R\in \mathrm{V}\wedge {\mathrm{Base}}_R\in \mathrm{V}\right)\to R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R$$
18	9 10 15 17	syl3anc	$$⊢\phi \to R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R$$
19		eqcom	$$⊢R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R\leftrightarrow R=R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R$$
20	19	imbi2i	$$⊢\left(\phi \to R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R\right)\leftrightarrow \left(\phi \to R=R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)$$
21	18 20	mpbi	$$⊢\phi \to R=R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R$$
22	21	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)$$
23	2 22	eqtrid	$$⊢\phi \to P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)$$
24	23	fveq2d	$$⊢\phi \to {\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}$$
25	4 24	eqtrid	$$⊢\phi \to U={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}$$
26	1 12	evl1fval1	$$⊢O=R{\mathrm{evalSub}}_1{\mathrm{Base}}_R$$
27	26	a1i	$$⊢\phi \to O=R{\mathrm{evalSub}}_1{\mathrm{Base}}_R$$
28	27	fveq1d	$$⊢\phi \to O\left(p\right)=\left(R{\mathrm{evalSub}}_1{\mathrm{Base}}_R\right)\left(p\right)$$
29	28	fveq1d	$$⊢\phi \to O\left(p\right)\left(X\right)=\left(R{\mathrm{evalSub}}_1{\mathrm{Base}}_R\right)\left(p\right)\left(X\right)$$
30	25 29	mpteq12dv	$$⊢\phi \to \left(p\in U⟼O\left(p\right)\left(X\right)\right)=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}⟼\left(R{\mathrm{evalSub}}_1{\mathrm{Base}}_R\right)\left(p\right)\left(X\right)\right)$$
31		eqid	$$⊢R{\mathrm{evalSub}}_1{\mathrm{Base}}_R=R{\mathrm{evalSub}}_1{\mathrm{Base}}_R$$
32		eqid	$$⊢{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)$$
33		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}$$
34	6 3	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
35		eqid	$$⊢\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}⟼\left(R{\mathrm{evalSub}}_1{\mathrm{Base}}_R\right)\left(p\right)\left(X\right)\right)=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}⟼\left(R{\mathrm{evalSub}}_1{\mathrm{Base}}_R\right)\left(p\right)\left(X\right)\right)$$
36	31 32 12 33 5 14 34 35	evls1maprhm	$$⊢\phi \to \left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)}⟼\left(R{\mathrm{evalSub}}_1{\mathrm{Base}}_R\right)\left(p\right)\left(X\right)\right)\in \left({\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\mathrm{RingHom}R\right)$$
37	30 36	eqeltrd	$$⊢\phi \to \left(p\in U⟼O\left(p\right)\left(X\right)\right)\in \left({\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\mathrm{RingHom}R\right)$$
38	2	a1i	$$⊢\phi \to P={\mathrm{Poly}}_1\left(R\right)$$
39	18	eqcomd	$$⊢\phi \to R=R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R$$
40	39	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)$$
41	38 40	eqtr2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)=P$$
42	41	oveq1d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\mathrm{RingHom}R=P\mathrm{RingHom}R$$
43	37 42	eleqtrd	$$⊢\phi \to \left(p\in U⟼O\left(p\right)\left(X\right)\right)\in \left(P\mathrm{RingHom}R\right)$$
44	8 43	eqeltrd	$$⊢\phi \to F\in \left(P\mathrm{RingHom}R\right)$$