evlsmaprhm

Description: The function F mapping polynomials p to their subring evaluation at a given point X is a ring homomorphism. Compare evls1maprhm . (Contributed by SN, 12-Mar-2025)

	Ref	Expression
Hypotheses	evlsmaprhm.q	$⊢ Q = (I evalSub R) (S)$
	evlsmaprhm.p	$⊢ P = I mPoly U$
	evlsmaprhm.u	$⊢ U = R ↾_{𝑠} S$
	evlsmaprhm.b	$⊢ B = {Base}_{P}$
	evlsmaprhm.k	$⊢ K = {Base}_{R}$
	evlsmaprhm.f	$⊢ F = (p \in B ⟼ Q (p) (A))$
	evlsmaprhm.i	$⊢ φ \to I \in V$
	evlsmaprhm.r	$⊢ φ \to R \in CRing$
	evlsmaprhm.s	$⊢ φ \to S \in SubRing (R)$
	evlsmaprhm.a	$⊢ φ \to A \in (K^{I})$
Assertion	evlsmaprhm	$⊢ φ \to F \in (P RingHom R)$

Proof

Step	Hyp	Ref	Expression
1		evlsmaprhm.q	$⊢ Q = (I evalSub R) (S)$
2		evlsmaprhm.p	$⊢ P = I mPoly U$
3		evlsmaprhm.u	$⊢ U = R ↾_{𝑠} S$
4		evlsmaprhm.b	$⊢ B = {Base}_{P}$
5		evlsmaprhm.k	$⊢ K = {Base}_{R}$
6		evlsmaprhm.f	$⊢ F = (p \in B ⟼ Q (p) (A))$
7		evlsmaprhm.i	$⊢ φ \to I \in V$
8		evlsmaprhm.r	$⊢ φ \to R \in CRing$
9		evlsmaprhm.s	$⊢ φ \to S \in SubRing (R)$
10		evlsmaprhm.a	$⊢ φ \to A \in (K^{I})$
11		eqid	$⊢ 1_{P} = 1_{P}$
12		eqid	$⊢ 1_{R} = 1_{R}$
13		eqid	$⊢ \cdot_{P} = \cdot_{P}$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15	3	subrgring	$⊢ S \in SubRing (R) \to U \in Ring$
16	9 15	syl	$⊢ φ \to U \in Ring$
17	2 7 16	mplringd	$⊢ φ \to P \in Ring$
18	8	crngringd	$⊢ φ \to R \in Ring$
19		fveq2	$⊢ p = 1_{P} \to Q (p) = Q (1_{P})$
20	19	fveq1d	$⊢ p = 1_{P} \to Q (p) (A) = Q (1_{P}) (A)$
21	4 11	ringidcl	$⊢ P \in Ring \to 1_{P} \in B$
22	17 21	syl	$⊢ φ \to 1_{P} \in B$
23		fvexd	$⊢ φ \to Q (1_{P}) (A) \in V$
24	6 20 22 23	fvmptd3	$⊢ φ \to F (1_{P}) = Q (1_{P}) (A)$
25		eqid	$⊢ algSc (P) = algSc (P)$
26		eqid	$⊢ 1_{U} = 1_{U}$
27	2 25 26 11 7 16	mplascl1	$⊢ φ \to algSc (P) (1_{U}) = 1_{P}$
28	27	eqcomd	$⊢ φ \to 1_{P} = algSc (P) (1_{U})$
29	28	fveq2d	$⊢ φ \to Q (1_{P}) = Q (algSc (P) (1_{U}))$
30	29	fveq1d	$⊢ φ \to Q (1_{P}) (A) = Q (algSc (P) (1_{U})) (A)$
31	3 12	subrg1	$⊢ S \in SubRing (R) \to 1_{R} = 1_{U}$
32	9 31	syl	$⊢ φ \to 1_{R} = 1_{U}$
33	12	subrg1cl	$⊢ S \in SubRing (R) \to 1_{R} \in S$
34	9 33	syl	$⊢ φ \to 1_{R} \in S$
35	32 34	eqeltrrd	$⊢ φ \to 1_{U} \in S$
36	1 2 3 5 4 25 7 8 9 35 10	evlsscaval	$⊢ φ \to (algSc (P) (1_{U}) \in B \land Q (algSc (P) (1_{U})) (A) = 1_{U})$
37	36	simprd	$⊢ φ \to Q (algSc (P) (1_{U})) (A) = 1_{U}$
38	37 32	eqtr4d	$⊢ φ \to Q (algSc (P) (1_{U})) (A) = 1_{R}$
39	24 30 38	3eqtrd	$⊢ φ \to F (1_{P}) = 1_{R}$
40	7	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to I \in V$
41	8	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to R \in CRing$
42	9	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to S \in SubRing (R)$
43	10	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to A \in (K^{I})$
44		simprl	$⊢ (φ \land (q \in B \land r \in B)) \to q \in B$
45		eqidd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (q) (A) = Q (q) (A)$
46	44 45	jca	$⊢ (φ \land (q \in B \land r \in B)) \to (q \in B \land Q (q) (A) = Q (q) (A))$
47		simprr	$⊢ (φ \land (q \in B \land r \in B)) \to r \in B$
48		eqidd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (r) (A) = Q (r) (A)$
49	47 48	jca	$⊢ (φ \land (q \in B \land r \in B)) \to (r \in B \land Q (r) (A) = Q (r) (A))$
50	1 2 3 5 4 40 41 42 43 46 49 13 14	evlsmulval	$⊢ (φ \land (q \in B \land r \in B)) \to (q \cdot_{P} r \in B \land Q (q \cdot_{P} r) (A) = Q (q) (A) \cdot_{R} Q (r) (A))$
51	50	simprd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (q \cdot_{P} r) (A) = Q (q) (A) \cdot_{R} Q (r) (A)$
52		fveq2	$⊢ p = q \cdot_{P} r \to Q (p) = Q (q \cdot_{P} r)$
53	52	fveq1d	$⊢ p = q \cdot_{P} r \to Q (p) (A) = Q (q \cdot_{P} r) (A)$
54	17	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to P \in Ring$
55	4 13 54 44 47	ringcld	$⊢ (φ \land (q \in B \land r \in B)) \to q \cdot_{P} r \in B$
56		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (q \cdot_{P} r) (A) \in V$
57	6 53 55 56	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to F (q \cdot_{P} r) = Q (q \cdot_{P} r) (A)$
58		fveq2	$⊢ p = q \to Q (p) = Q (q)$
59	58	fveq1d	$⊢ p = q \to Q (p) (A) = Q (q) (A)$
60		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (q) (A) \in V$
61	6 59 44 60	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to F (q) = Q (q) (A)$
62		fveq2	$⊢ p = r \to Q (p) = Q (r)$
63	62	fveq1d	$⊢ p = r \to Q (p) (A) = Q (r) (A)$
64		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (r) (A) \in V$
65	6 63 47 64	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to F (r) = Q (r) (A)$
66	61 65	oveq12d	$⊢ (φ \land (q \in B \land r \in B)) \to F (q) \cdot_{R} F (r) = Q (q) (A) \cdot_{R} Q (r) (A)$
67	51 57 66	3eqtr4d	$⊢ (φ \land (q \in B \land r \in B)) \to F (q \cdot_{P} r) = F (q) \cdot_{R} F (r)$
68		eqid	$⊢ +_{P} = +_{P}$
69		eqid	$⊢ +_{R} = +_{R}$
70	7	adantr	$⊢ (φ \land p \in B) \to I \in V$
71	8	adantr	$⊢ (φ \land p \in B) \to R \in CRing$
72	9	adantr	$⊢ (φ \land p \in B) \to S \in SubRing (R)$
73		simpr	$⊢ (φ \land p \in B) \to p \in B$
74	10	adantr	$⊢ (φ \land p \in B) \to A \in (K^{I})$
75	1 2 3 4 5 70 71 72 73 74	evlscl	$⊢ (φ \land p \in B) \to Q (p) (A) \in K$
76	75 6	fmptd	$⊢ φ \to F : B ⟶ K$
77	1 2 3 5 4 40 41 42 43 46 49 68 69	evlsaddval	$⊢ (φ \land (q \in B \land r \in B)) \to (q +_{P} r \in B \land Q (q +_{P} r) (A) = Q (q) (A) +_{R} Q (r) (A))$
78	77	simprd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (q +_{P} r) (A) = Q (q) (A) +_{R} Q (r) (A)$
79		fveq2	$⊢ p = q +_{P} r \to Q (p) = Q (q +_{P} r)$
80	79	fveq1d	$⊢ p = q +_{P} r \to Q (p) (A) = Q (q +_{P} r) (A)$
81	17	ringgrpd	$⊢ φ \to P \in Grp$
82	81	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to P \in Grp$
83	4 68 82 44 47	grpcld	$⊢ (φ \land (q \in B \land r \in B)) \to q +_{P} r \in B$
84		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to Q (q +_{P} r) (A) \in V$
85	6 80 83 84	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to F (q +_{P} r) = Q (q +_{P} r) (A)$
86	61 65	oveq12d	$⊢ (φ \land (q \in B \land r \in B)) \to F (q) +_{R} F (r) = Q (q) (A) +_{R} Q (r) (A)$
87	78 85 86	3eqtr4d	$⊢ (φ \land (q \in B \land r \in B)) \to F (q +_{P} r) = F (q) +_{R} F (r)$
88	4 11 12 13 14 17 18 39 67 5 68 69 76 87	isrhmd	$⊢ φ \to F \in (P RingHom R)$

Metamath Proof Explorer

Theorem evlsmaprhm

Proof