Theorem evls1maprhm

Description: The function F mapping polynomials p to their subring evaluation at a given point X is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		evls1maprhm.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3		evls1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evls1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
5		evls1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		evls1maprhm.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7		evls1maprhm.y	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		evls1maprhm.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
9		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
12		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
14	13	subrgcrng	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑆 ) ∈ CRing )
15	5 6 14	syl2anc	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ CRing )
16	2	ply1crng	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ CRing → 𝑃 ∈ CRing )
17	15 16	syl	⊢ ( 𝜑 → 𝑃 ∈ CRing )
18	17	crngringd	⊢ ( 𝜑 → 𝑃 ∈ Ring )
19	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
20		fveq2	⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) )
21	20	fveq1d	⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) )
22	4 9	ringidcl	⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
23	18 22	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
24		fvexd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) ∈ V )
25	8 21 23 24	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) )
26	13 10	subrg1	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
27	6 26	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
28	27	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
29	15	crngringd	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
30		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
31		eqid	⊢ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) )
32	2 30 31 9	ply1scl1	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 1r ‘ 𝑃 ) )
33	29 32	syl	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 1r ‘ 𝑃 ) )
34	28 33	eqtr2d	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) )
35	34	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
36	35	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) )
37	10	subrg1cl	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
38	6 37	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
39	1 2 13 3 30 5 6 38 7	evls1scafv	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 1r ‘ 𝑅 ) )
40	25 36 39	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑅 ) )
41	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑅 ∈ CRing )
42	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
43		simprl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑞 ∈ 𝑈 )
44		simprr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑟 ∈ 𝑈 )
45	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
46	1 3 2 13 4 11 12 41 42 43 44 45	evls1muld	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
47		fveq2	⊢ ( 𝑝 = ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) )
48	47	fveq1d	⊢ ( 𝑝 = ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
49	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑃 ∈ Ring )
50	4 11 49 43 44	ringcld	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ∈ 𝑈 )
51		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) ∈ V )
52	8 48 50 51	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
53		fveq2	⊢ ( 𝑝 = 𝑞 → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ 𝑞 ) )
54	53	fveq1d	⊢ ( 𝑝 = 𝑞 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) )
55		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ∈ V )
56	8 54 43 55	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑞 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) )
57		fveq2	⊢ ( 𝑝 = 𝑟 → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ 𝑟 ) )
58	57	fveq1d	⊢ ( 𝑝 = 𝑟 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) )
59		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ∈ V )
60	8 58 44 59	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑟 ) = ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) )
61	56 60	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝐹 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
62	46 52 61	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) )
63		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
64		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
65		eqid	⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
66	1 3 2 13 4 65 5 6	ressply1evl	⊢ ( 𝜑 → 𝑂 = ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) )
67	66	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑂 = ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) )
68	67	fveq1d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑂 ‘ 𝑝 ) = ( ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝑝 ) )
69		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
70	69	fvresd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝑝 ) = ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) )
71	68 70	eqtrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑂 ‘ 𝑝 ) = ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) )
72	71	fveq1d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) ‘ 𝑋 ) )
73		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
74		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
75	5	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑅 ∈ CRing )
76	7	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
77		eqid	⊢ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) )
78		eqid	⊢ ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
79	73 13 2 4 6 77 78 74	ressply1bas2	⊢ ( 𝜑 → 𝑈 = ( ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) )
80		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑅 ) )
81	79 80	eqsstrdi	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
82	81	sselda	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
83	65 73 3 74 75 76 82	fveval1fvcl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) ‘ 𝑋 ) ∈ 𝐵 )
84	72 83	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ∈ 𝐵 )
85	84 8	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ 𝐵 )
86	1 3 2 13 4 63 64 41 42 43 44 45	evls1addd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
87		fveq2	⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) )
88	87	fveq1d	⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
89	49	ringgrpd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑃 ∈ Grp )
90	4 63 89 43 44	grpcld	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ∈ 𝑈 )
91		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) ∈ V )
92	8 88 90 91	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
93	56 60	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝐹 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
94	86 92 93	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) )
95	4 9 10 11 12 18 19 40 62 3 63 64 85 94	isrhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )