Theorem evls1maplmhm

Description: The function F mapping polynomials p to their subring evaluation at a given point A is a module homomorphism, when considering the subring algebra. (Contributed by Thierry Arnoux, 25-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	⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
	evls1maplmhm.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑆 )
Assertion	evls1maplmhm	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 LMHom 𝐴 ) )

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		evls1maplmhm.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑆 )
10		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
11	10	subrgring	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
12	6 11	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
13	2	ply1lmod	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ LMod )
14	12 13	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
15	9	sralmod	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ LMod )
16	6 15	syl	⊢ ( 𝜑 → 𝐴 ∈ LMod )
17	1 2 3 4 5 6 7 8	evls1maprhm	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )
18		rhmghm	⊢ ( 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) → 𝐹 ∈ ( 𝑃 GrpHom 𝑅 ) )
19	17 18	syl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 GrpHom 𝑅 ) )
20	4	a1i	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑃 ) )
21	3	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
22	9	a1i	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑆 ) )
23	3	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
24	6 23	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
25	24 3	sseqtrdi	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
26	22 25	srabase	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐴 ) )
27	3 26	eqtrid	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐴 ) )
28		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) )
29	22 25	sraaddg	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐴 ) )
30	29	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
31	20 21 20 27 28 30	ghmpropd	⊢ ( 𝜑 → ( 𝑃 GrpHom 𝑅 ) = ( 𝑃 GrpHom 𝐴 ) )
32	19 31	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 GrpHom 𝐴 ) )
33	22 25	srasca	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
34		ovex	⊢ ( 𝑅 ↾s 𝑆 ) ∈ V
35	2	ply1sca	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ V → ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 ) )
36	34 35	mp1i	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 ) )
37	33 36	eqtr3d	⊢ ( 𝜑 → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝑃 ) )
38		fveq2	⊢ ( 𝑝 = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) )
39	38	fveq1d	⊢ ( 𝑝 = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ‘ 𝑋 ) )
40	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑃 ∈ LMod )
41		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
42		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
43		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
44		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
45		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
46	4 43 44 45	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ 𝑈 )
47	40 41 42 46	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ 𝑈 )
48		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑂 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ‘ 𝑋 ) ∈ V )
49	8 39 47 48	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) = ( ( 𝑂 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ‘ 𝑋 ) )
50		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
51	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑅 ∈ CRing )
52	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
53	10 3	ressbas2	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
54	24 53	syl	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
55	36	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
56	54 55	eqtr2d	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = 𝑆 )
57	56	eqimssd	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⊆ 𝑆 )
58	57	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → 𝑘 ∈ 𝑆 )
59	58	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑘 ∈ 𝑆 )
60	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
61	1 3 2 10 4 44 50 51 52 59 42 60	evls1vsca	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑂 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ‘ 𝑋 ) = ( 𝑘 ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑥 ) ‘ 𝑋 ) ) )
62	22 25	sravsca	⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ 𝐴 ) )
63	62	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ 𝐴 ) )
64		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑘 = 𝑘 )
65		fveq2	⊢ ( 𝑝 = 𝑥 → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ 𝑥 ) )
66	65	fveq1d	⊢ ( 𝑝 = 𝑥 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ 𝑥 ) ‘ 𝑋 ) )
67		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑥 ) ‘ 𝑋 ) ∈ V )
68	8 66 42 67	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝑥 ) ‘ 𝑋 ) )
69	68	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑥 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑥 ) )
70	63 64 69	oveq123d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝑘 ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑥 ) ‘ 𝑋 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑥 ) ) )
71	49 61 70	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑥 ) ) )
72	71	anasss	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑥 ) ) )
73	72	ralrimivva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑥 ) ) )
74		eqid	⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
75		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
76	43 74 45 4 44 75	islmhm	⊢ ( 𝐹 ∈ ( 𝑃 LMHom 𝐴 ) ↔ ( ( 𝑃 ∈ LMod ∧ 𝐴 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑃 GrpHom 𝐴 ) ∧ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝑃 ) ∧ ∀ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
77	76	biimpri	⊢ ( ( ( 𝑃 ∈ LMod ∧ 𝐴 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑃 GrpHom 𝐴 ) ∧ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝑃 ) ∧ ∀ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑥 ) ) ) ) → 𝐹 ∈ ( 𝑃 LMHom 𝐴 ) )
78	14 16 32 37 73 77	syl23anc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 LMHom 𝐴 ) )