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	$⊢ 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))$
Assertion	evls1maprhm	$⊢ φ \to F \in (P RingHom R)$

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		eqid	$⊢ 1_{P} = 1_{P}$
10		eqid	$⊢ 1_{R} = 1_{R}$
11		eqid	$⊢ \cdot_{P} = \cdot_{P}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
14	13	subrgcrng	$⊢ (R \in CRing \land S \in SubRing (R)) \to R ↾_{𝑠} S \in CRing$
15	5 6 14	syl2anc	$⊢ φ \to R ↾_{𝑠} S \in CRing$
16	2	ply1crng	$⊢ R ↾_{𝑠} S \in CRing \to P \in CRing$
17	15 16	syl	$⊢ φ \to P \in CRing$
18	17	crngringd	$⊢ φ \to P \in Ring$
19	5	crngringd	$⊢ φ \to R \in Ring$
20		fveq2	$⊢ p = 1_{P} \to O (p) = O (1_{P})$
21	20	fveq1d	$⊢ p = 1_{P} \to O (p) (X) = O (1_{P}) (X)$
22	4 9	ringidcl	$⊢ P \in Ring \to 1_{P} \in U$
23	18 22	syl	$⊢ φ \to 1_{P} \in U$
24		fvexd	$⊢ φ \to O (1_{P}) (X) \in V$
25	8 21 23 24	fvmptd3	$⊢ φ \to F (1_{P}) = O (1_{P}) (X)$
26	13 10	subrg1	$⊢ S \in SubRing (R) \to 1_{R} = 1_{(R ↾_{𝑠} S)}$
27	6 26	syl	$⊢ φ \to 1_{R} = 1_{(R ↾_{𝑠} S)}$
28	27	fveq2d	$⊢ φ \to algSc (P) (1_{R}) = algSc (P) (1_{(R ↾_{𝑠} S)})$
29	15	crngringd	$⊢ φ \to R ↾_{𝑠} S \in Ring$
30		eqid	$⊢ algSc (P) = algSc (P)$
31		eqid	$⊢ 1_{(R ↾_{𝑠} S)} = 1_{(R ↾_{𝑠} S)}$
32	2 30 31 9	ply1scl1	$⊢ R ↾_{𝑠} S \in Ring \to algSc (P) (1_{(R ↾_{𝑠} S)}) = 1_{P}$
33	29 32	syl	$⊢ φ \to algSc (P) (1_{(R ↾_{𝑠} S)}) = 1_{P}$
34	28 33	eqtr2d	$⊢ φ \to 1_{P} = algSc (P) (1_{R})$
35	34	fveq2d	$⊢ φ \to O (1_{P}) = O (algSc (P) (1_{R}))$
36	35	fveq1d	$⊢ φ \to O (1_{P}) (X) = O (algSc (P) (1_{R})) (X)$
37	10	subrg1cl	$⊢ S \in SubRing (R) \to 1_{R} \in S$
38	6 37	syl	$⊢ φ \to 1_{R} \in S$
39	1 2 13 3 30 5 6 38 7	evls1scafv	$⊢ φ \to O (algSc (P) (1_{R})) (X) = 1_{R}$
40	25 36 39	3eqtrd	$⊢ φ \to F (1_{P}) = 1_{R}$
41	5	adantr	$⊢ (φ \land (q \in U \land r \in U)) \to R \in CRing$
42	6	adantr	$⊢ (φ \land (q \in U \land r \in U)) \to S \in SubRing (R)$
43		simprl	$⊢ (φ \land (q \in U \land r \in U)) \to q \in U$
44		simprr	$⊢ (φ \land (q \in U \land r \in U)) \to r \in U$
45	7	adantr	$⊢ (φ \land (q \in U \land r \in U)) \to X \in B$
46	1 3 2 13 4 11 12 41 42 43 44 45	evls1muld	$⊢ (φ \land (q \in U \land r \in U)) \to O (q \cdot_{P} r) (X) = O (q) (X) \cdot_{R} O (r) (X)$
47		fveq2	$⊢ p = q \cdot_{P} r \to O (p) = O (q \cdot_{P} r)$
48	47	fveq1d	$⊢ p = q \cdot_{P} r \to O (p) (X) = O (q \cdot_{P} r) (X)$
49	18	adantr	$⊢ (φ \land (q \in U \land r \in U)) \to P \in Ring$
50	4 11 49 43 44	ringcld	$⊢ (φ \land (q \in U \land r \in U)) \to q \cdot_{P} r \in U$
51		fvexd	$⊢ (φ \land (q \in U \land r \in U)) \to O (q \cdot_{P} r) (X) \in V$
52	8 48 50 51	fvmptd3	$⊢ (φ \land (q \in U \land r \in U)) \to F (q \cdot_{P} r) = O (q \cdot_{P} r) (X)$
53		fveq2	$⊢ p = q \to O (p) = O (q)$
54	53	fveq1d	$⊢ p = q \to O (p) (X) = O (q) (X)$
55		fvexd	$⊢ (φ \land (q \in U \land r \in U)) \to O (q) (X) \in V$
56	8 54 43 55	fvmptd3	$⊢ (φ \land (q \in U \land r \in U)) \to F (q) = O (q) (X)$
57		fveq2	$⊢ p = r \to O (p) = O (r)$
58	57	fveq1d	$⊢ p = r \to O (p) (X) = O (r) (X)$
59		fvexd	$⊢ (φ \land (q \in U \land r \in U)) \to O (r) (X) \in V$
60	8 58 44 59	fvmptd3	$⊢ (φ \land (q \in U \land r \in U)) \to F (r) = O (r) (X)$
61	56 60	oveq12d	$⊢ (φ \land (q \in U \land r \in U)) \to F (q) \cdot_{R} F (r) = O (q) (X) \cdot_{R} O (r) (X)$
62	46 52 61	3eqtr4d	$⊢ (φ \land (q \in U \land r \in U)) \to F (q \cdot_{P} r) = F (q) \cdot_{R} F (r)$
63		eqid	$⊢ +_{P} = +_{P}$
64		eqid	$⊢ +_{R} = +_{R}$
65		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
66	1 3 2 13 4 65 5 6	ressply1evl	$⊢ φ \to O = {{eval}_{1} (R) ↾}_{U}$
67	66	adantr	$⊢ (φ \land p \in U) \to O = {{eval}_{1} (R) ↾}_{U}$
68	67	fveq1d	$⊢ (φ \land p \in U) \to O (p) = ({{eval}_{1} (R) ↾}_{U}) (p)$
69		simpr	$⊢ (φ \land p \in U) \to p \in U$
70	69	fvresd	$⊢ (φ \land p \in U) \to ({{eval}_{1} (R) ↾}_{U}) (p) = {eval}_{1} (R) (p)$
71	68 70	eqtrd	$⊢ (φ \land p \in U) \to O (p) = {eval}_{1} (R) (p)$
72	71	fveq1d	$⊢ (φ \land p \in U) \to O (p) (X) = {eval}_{1} (R) (p) (X)$
73		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
74		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
75	5	adantr	$⊢ (φ \land p \in U) \to R \in CRing$
76	7	adantr	$⊢ (φ \land p \in U) \to X \in B$
77		eqid	$⊢ {PwSer}_{1} (R ↾_{𝑠} S) = {PwSer}_{1} (R ↾_{𝑠} S)$
78		eqid	$⊢ {Base}_{{PwSer}_{1} (R ↾_{𝑠} S)} = {Base}_{{PwSer}_{1} (R ↾_{𝑠} S)}$
79	73 13 2 4 6 77 78 74	ressply1bas2	$⊢ φ \to U = {Base}_{{PwSer}_{1} (R ↾_{𝑠} S)} \cap {Base}_{{Poly}_{1} (R)}$
80		inss2	$⊢ {Base}_{{PwSer}_{1} (R ↾_{𝑠} S)} \cap {Base}_{{Poly}_{1} (R)} \subseteq {Base}_{{Poly}_{1} (R)}$
81	79 80	eqsstrdi	$⊢ φ \to U \subseteq {Base}_{{Poly}_{1} (R)}$
82	81	sselda	$⊢ (φ \land p \in U) \to p \in {Base}_{{Poly}_{1} (R)}$
83	65 73 3 74 75 76 82	fveval1fvcl	$⊢ (φ \land p \in U) \to {eval}_{1} (R) (p) (X) \in B$
84	72 83	eqeltrd	$⊢ (φ \land p \in U) \to O (p) (X) \in B$
85	84 8	fmptd	$⊢ φ \to F : U ⟶ B$
86	1 3 2 13 4 63 64 41 42 43 44 45	evls1addd	$⊢ (φ \land (q \in U \land r \in U)) \to O (q +_{P} r) (X) = O (q) (X) +_{R} O (r) (X)$
87		fveq2	$⊢ p = q +_{P} r \to O (p) = O (q +_{P} r)$
88	87	fveq1d	$⊢ p = q +_{P} r \to O (p) (X) = O (q +_{P} r) (X)$
89	49	ringgrpd	$⊢ (φ \land (q \in U \land r \in U)) \to P \in Grp$
90	4 63 89 43 44	grpcld	$⊢ (φ \land (q \in U \land r \in U)) \to q +_{P} r \in U$
91		fvexd	$⊢ (φ \land (q \in U \land r \in U)) \to O (q +_{P} r) (X) \in V$
92	8 88 90 91	fvmptd3	$⊢ (φ \land (q \in U \land r \in U)) \to F (q +_{P} r) = O (q +_{P} r) (X)$
93	56 60	oveq12d	$⊢ (φ \land (q \in U \land r \in U)) \to F (q) +_{R} F (r) = O (q) (X) +_{R} O (r) (X)$
94	86 92 93	3eqtr4d	$⊢ (φ \land (q \in U \land r \in U)) \to F (q +_{P} r) = F (q) +_{R} F (r)$
95	4 9 10 11 12 18 19 40 62 3 63 64 85 94	isrhmd	$⊢ φ \to F \in (P RingHom R)$

Metamath Proof Explorer

Theorem evls1maprhm

Proof