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	$⊢ O = R {evalSub}_{1} S$
	evls1maprhm.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
	evls1maprhm.b	$⊢ B = {Base}_{R}$
	evls1maprhm.u	$⊢ U = {Base}_{P}$
	evls1maprhm.r	$⊢ φ \to R \in CRing$
	evls1maprhm.s	$⊢ φ \to S \in SubRing (R)$
	evls1maprhm.y	$⊢ φ \to X \in B$
	evls1maprhm.f	$⊢ F = (p \in U ⟼ O (p) (X))$
	evls1maplmhm.1	$⊢ A = subringAlg (R) (S)$
Assertion	evls1maplmhm	$⊢ φ \to F \in (P LMHom A)$

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	$⊢ O = R {evalSub}_{1} S$
2		evls1maprhm.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
3		evls1maprhm.b	$⊢ B = {Base}_{R}$
4		evls1maprhm.u	$⊢ U = {Base}_{P}$
5		evls1maprhm.r	$⊢ φ \to R \in CRing$
6		evls1maprhm.s	$⊢ φ \to S \in SubRing (R)$
7		evls1maprhm.y	$⊢ φ \to X \in B$
8		evls1maprhm.f	$⊢ F = (p \in U ⟼ O (p) (X))$
9		evls1maplmhm.1	$⊢ A = subringAlg (R) (S)$
10		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
11	10	subrgring	$⊢ S \in SubRing (R) \to R ↾_{𝑠} S \in Ring$
12	6 11	syl	$⊢ φ \to R ↾_{𝑠} S \in Ring$
13	2	ply1lmod	$⊢ R ↾_{𝑠} S \in Ring \to P \in LMod$
14	12 13	syl	$⊢ φ \to P \in LMod$
15	9	sralmod	$⊢ S \in SubRing (R) \to A \in LMod$
16	6 15	syl	$⊢ φ \to A \in LMod$
17	1 2 3 4 5 6 7 8	evls1maprhm	$⊢ φ \to F \in (P RingHom R)$
18		rhmghm	$⊢ F \in (P RingHom R) \to F \in (P GrpHom R)$
19	17 18	syl	$⊢ φ \to F \in (P GrpHom R)$
20	4	a1i	$⊢ φ \to U = {Base}_{P}$
21	3	a1i	$⊢ φ \to B = {Base}_{R}$
22	9	a1i	$⊢ φ \to A = subringAlg (R) (S)$
23	3	subrgss	$⊢ S \in SubRing (R) \to S \subseteq B$
24	6 23	syl	$⊢ φ \to S \subseteq B$
25	24 3	sseqtrdi	$⊢ φ \to S \subseteq {Base}_{R}$
26	22 25	srabase	$⊢ φ \to {Base}_{R} = {Base}_{A}$
27	3 26	eqtrid	$⊢ φ \to B = {Base}_{A}$
28		eqidd	$⊢ (φ \land (x \in U \land y \in U)) \to x +_{P} y = x +_{P} y$
29	22 25	sraaddg	$⊢ φ \to +_{R} = +_{A}$
30	29	oveqdr	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{A} y$
31	20 21 20 27 28 30	ghmpropd	$⊢ φ \to P GrpHom R = P GrpHom A$
32	19 31	eleqtrd	$⊢ φ \to F \in (P GrpHom A)$
33	22 25	srasca	$⊢ φ \to R ↾_{𝑠} S = Scalar (A)$
34		ovex	$⊢ R ↾_{𝑠} S \in V$
35	2	ply1sca	$⊢ R ↾_{𝑠} S \in V \to R ↾_{𝑠} S = Scalar (P)$
36	34 35	mp1i	$⊢ φ \to R ↾_{𝑠} S = Scalar (P)$
37	33 36	eqtr3d	$⊢ φ \to Scalar (A) = Scalar (P)$
38		fveq2	$⊢ p = k \cdot_{P} x \to O (p) = O (k \cdot_{P} x)$
39	38	fveq1d	$⊢ p = k \cdot_{P} x \to O (p) (X) = O (k \cdot_{P} x) (X)$
40	14	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to P \in LMod$
41		simplr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to k \in {Base}_{Scalar (P)}$
42		simpr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to x \in U$
43		eqid	$⊢ Scalar (P) = Scalar (P)$
44		eqid	$⊢ \cdot_{P} = \cdot_{P}$
45		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
46	4 43 44 45	lmodvscl	$⊢ (P \in LMod \land k \in {Base}_{Scalar (P)} \land x \in U) \to k \cdot_{P} x \in U$
47	40 41 42 46	syl3anc	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to k \cdot_{P} x \in U$
48		fvexd	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to O (k \cdot_{P} x) (X) \in V$
49	8 39 47 48	fvmptd3	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to F (k \cdot_{P} x) = O (k \cdot_{P} x) (X)$
50		eqid	$⊢ \cdot_{R} = \cdot_{R}$
51	5	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to R \in CRing$
52	6	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to S \in SubRing (R)$
53	10 3	ressbas2	$⊢ S \subseteq B \to S = {Base}_{(R ↾_{𝑠} S)}$
54	24 53	syl	$⊢ φ \to S = {Base}_{(R ↾_{𝑠} S)}$
55	36	fveq2d	$⊢ φ \to {Base}_{(R ↾_{𝑠} S)} = {Base}_{Scalar (P)}$
56	54 55	eqtr2d	$⊢ φ \to {Base}_{Scalar (P)} = S$
57	56	eqimssd	$⊢ φ \to {Base}_{Scalar (P)} \subseteq S$
58	57	sselda	$⊢ (φ \land k \in {Base}_{Scalar (P)}) \to k \in S$
59	58	adantr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to k \in S$
60	7	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to X \in B$
61	1 3 2 10 4 44 50 51 52 59 42 60	evls1vsca	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to O (k \cdot_{P} x) (X) = k \cdot_{R} O (x) (X)$
62	22 25	sravsca	$⊢ φ \to \cdot_{R} = \cdot_{A}$
63	62	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to \cdot_{R} = \cdot_{A}$
64		eqidd	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to k = k$
65		fveq2	$⊢ p = x \to O (p) = O (x)$
66	65	fveq1d	$⊢ p = x \to O (p) (X) = O (x) (X)$
67		fvexd	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to O (x) (X) \in V$
68	8 66 42 67	fvmptd3	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to F (x) = O (x) (X)$
69	68	eqcomd	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to O (x) (X) = F (x)$
70	63 64 69	oveq123d	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to k \cdot_{R} O (x) (X) = k \cdot_{A} F (x)$
71	49 61 70	3eqtrd	$⊢ ((φ \land k \in {Base}_{Scalar (P)}) \land x \in U) \to F (k \cdot_{P} x) = k \cdot_{A} F (x)$
72	71	anasss	$⊢ (φ \land (k \in {Base}_{Scalar (P)} \land x \in U)) \to F (k \cdot_{P} x) = k \cdot_{A} F (x)$
73	72	ralrimivva	$⊢ φ \to \forall k \in {Base}_{Scalar (P)} \forall x \in U F (k \cdot_{P} x) = k \cdot_{A} F (x)$
74		eqid	$⊢ Scalar (A) = Scalar (A)$
75		eqid	$⊢ \cdot_{A} = \cdot_{A}$
76	43 74 45 4 44 75	islmhm	$⊢ F \in (P LMHom A) \leftrightarrow ((P \in LMod \land A \in LMod) \land (F \in (P GrpHom A) \land Scalar (A) = Scalar (P) \land \forall k \in {Base}_{Scalar (P)} \forall x \in U F (k \cdot_{P} x) = k \cdot_{A} F (x)))$
77	76	biimpri	$⊢ ((P \in LMod \land A \in LMod) \land (F \in (P GrpHom A) \land Scalar (A) = Scalar (P) \land \forall k \in {Base}_{Scalar (P)} \forall x \in U F (k \cdot_{P} x) = k \cdot_{A} F (x))) \to F \in (P LMHom A)$
78	14 16 32 37 73 77	syl23anc	$⊢ φ \to F \in (P LMHom A)$

Metamath Proof Explorer

Theorem evls1maplmhm

Proof