r1plmhm

Description: The univariate polynomial remainder function F is a module homomorphism. Its image ( F "s P ) is sometimes called the "ring of remainders". (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	r1plmhm.1	$⊢ P = {Poly}_{1} (R)$
	r1plmhm.2	$⊢ U = {Base}_{P}$
	r1plmhm.4	$⊢ E = {rem}_{1p} (R)$
	r1plmhm.5	$⊢ N = {Unic}_{1p} (R)$
	r1plmhm.6	$⊢ F = (f \in U ⟼ f E M)$
	r1plmhm.9	$⊢ φ \to R \in Ring$
	r1plmhm.10	$⊢ φ \to M \in N$
Assertion	r1plmhm	$⊢ φ \to F \in (P LMHom (F “_{𝑠} P))$

Proof

Step	Hyp	Ref	Expression
1		r1plmhm.1	$⊢ P = {Poly}_{1} (R)$
2		r1plmhm.2	$⊢ U = {Base}_{P}$
3		r1plmhm.4	$⊢ E = {rem}_{1p} (R)$
4		r1plmhm.5	$⊢ N = {Unic}_{1p} (R)$
5		r1plmhm.6	$⊢ F = (f \in U ⟼ f E M)$
6		r1plmhm.9	$⊢ φ \to R \in Ring$
7		r1plmhm.10	$⊢ φ \to M \in N$
8	6	adantr	$⊢ (φ \land f \in U) \to R \in Ring$
9		simpr	$⊢ (φ \land f \in U) \to f \in U$
10	7	adantr	$⊢ (φ \land f \in U) \to M \in N$
11	3 1 2 4	r1pcl	$⊢ (R \in Ring \land f \in U \land M \in N) \to f E M \in U$
12	8 9 10 11	syl3anc	$⊢ (φ \land f \in U) \to f E M \in U$
13	12 5	fmptd	$⊢ φ \to F : U ⟶ U$
14		eqid	$⊢ +_{P} = +_{P}$
15		anass	$⊢ ((φ \land a \in U) \land b \in U) \leftrightarrow (φ \land (a \in U \land b \in U))$
16	6	ad6antr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to R \in Ring$
17		simp-6r	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to a \in U$
18	7	ad6antr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to M \in N$
19		simplr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (a) = F (p)$
20		oveq1	$⊢ f = a \to f E M = a E M$
21		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to a E M \in V$
22	5 20 17 21	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (a) = a E M$
23		oveq1	$⊢ f = p \to f E M = p E M$
24		simp-4r	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to p \in U$
25		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to p E M \in V$
26	5 23 24 25	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (p) = p E M$
27	19 22 26	3eqtr3d	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to a E M = p E M$
28		simp-5r	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to b \in U$
29	1 2 4 3 16 17 18 27 14 24 28	r1padd1	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to (a +_{P} b) E M = (p +_{P} b) E M$
30		oveq1	$⊢ f = a +_{P} b \to f E M = (a +_{P} b) E M$
31	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
32	6 31	syl	$⊢ φ \to P \in Ring$
33	32	ringgrpd	$⊢ φ \to P \in Grp$
34	33	ad6antr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to P \in Grp$
35	2 14 34 17 28	grpcld	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to a +_{P} b \in U$
36		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to (a +_{P} b) E M \in V$
37	5 30 35 36	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (a +_{P} b) = (a +_{P} b) E M$
38		oveq1	$⊢ f = p +_{P} b \to f E M = (p +_{P} b) E M$
39	2 14 34 24 28	grpcld	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to p +_{P} b \in U$
40		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to (p +_{P} b) E M \in V$
41	5 38 39 40	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (p +_{P} b) = (p +_{P} b) E M$
42	29 37 41	3eqtr4d	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (a +_{P} b) = F (p +_{P} b)$
43	32	ringabld	$⊢ φ \to P \in Abel$
44	43	ad6antr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to P \in Abel$
45	2 14	ablcom	$⊢ (P \in Abel \land p \in U \land b \in U) \to p +_{P} b = b +_{P} p$
46	44 24 28 45	syl3anc	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to p +_{P} b = b +_{P} p$
47	46	fveq2d	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (p +_{P} b) = F (b +_{P} p)$
48	42 47	eqtrd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (a +_{P} b) = F (b +_{P} p)$
49		simpr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (b) = F (q)$
50		oveq1	$⊢ f = b \to f E M = b E M$
51		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to b E M \in V$
52	5 50 28 51	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (b) = b E M$
53		oveq1	$⊢ f = q \to f E M = q E M$
54		simpllr	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to q \in U$
55		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to q E M \in V$
56	5 53 54 55	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (q) = q E M$
57	49 52 56	3eqtr3d	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to b E M = q E M$
58	1 2 4 3 16 28 18 57 14 54 24	r1padd1	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to (b +_{P} p) E M = (q +_{P} p) E M$
59		oveq1	$⊢ f = b +_{P} p \to f E M = (b +_{P} p) E M$
60	2 14 34 28 24	grpcld	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to b +_{P} p \in U$
61		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to (b +_{P} p) E M \in V$
62	5 59 60 61	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (b +_{P} p) = (b +_{P} p) E M$
63		oveq1	$⊢ f = q +_{P} p \to f E M = (q +_{P} p) E M$
64	2 14 34 54 24	grpcld	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to q +_{P} p \in U$
65		ovexd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to (q +_{P} p) E M \in V$
66	5 63 64 65	fvmptd3	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (q +_{P} p) = (q +_{P} p) E M$
67	58 62 66	3eqtr4d	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (b +_{P} p) = F (q +_{P} p)$
68	2 14	ablcom	$⊢ (P \in Abel \land q \in U \land p \in U) \to q +_{P} p = p +_{P} q$
69	44 54 24 68	syl3anc	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to q +_{P} p = p +_{P} q$
70	69	fveq2d	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (q +_{P} p) = F (p +_{P} q)$
71	48 67 70	3eqtrd	$⊢ ((((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \land F (a) = F (p)) \land F (b) = F (q)) \to F (a +_{P} b) = F (p +_{P} q)$
72	71	expl	$⊢ ((((φ \land a \in U) \land b \in U) \land p \in U) \land q \in U) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a +_{P} b) = F (p +_{P} q))$
73	72	anasss	$⊢ (((φ \land a \in U) \land b \in U) \land (p \in U \land q \in U)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a +_{P} b) = F (p +_{P} q))$
74	15 73	sylanbr	$⊢ ((φ \land (a \in U \land b \in U)) \land (p \in U \land q \in U)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a +_{P} b) = F (p +_{P} q))$
75	74	3impa	$⊢ (φ \land (a \in U \land b \in U) \land (p \in U \land q \in U)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a +_{P} b) = F (p +_{P} q))$
76		eqid	$⊢ Scalar (P) = Scalar (P)$
77		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
78		simplr	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to F (a) = F (b)$
79		simpr2	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to a \in U$
80		ovexd	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to a E M \in V$
81	5 20 79 80	fvmptd3	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to F (a) = a E M$
82		simpr3	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to b \in U$
83		ovexd	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to b E M \in V$
84	5 50 82 83	fvmptd3	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to F (b) = b E M$
85	78 81 84	3eqtr3d	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to a E M = b E M$
86	85	oveq2d	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to k \cdot_{P} (a E M) = k \cdot_{P} (b E M)$
87	6	ad2antrr	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to R \in Ring$
88	7	ad2antrr	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to M \in N$
89		eqid	$⊢ \cdot_{P} = \cdot_{P}$
90		eqid	$⊢ {Base}_{R} = {Base}_{R}$
91		simpr1	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to k \in {Base}_{Scalar (P)}$
92	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
93	6 92	syl	$⊢ φ \to R = Scalar (P)$
94	93	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (P)}$
95	94	ad2antrr	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to {Base}_{R} = {Base}_{Scalar (P)}$
96	91 95	eleqtrrd	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to k \in {Base}_{R}$
97	1 2 4 3 87 79 88 89 90 96	r1pvsca	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to (k \cdot_{P} a) E M = k \cdot_{P} (a E M)$
98	1 2 4 3 87 82 88 89 90 96	r1pvsca	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to (k \cdot_{P} b) E M = k \cdot_{P} (b E M)$
99	86 97 98	3eqtr4d	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to (k \cdot_{P} a) E M = (k \cdot_{P} b) E M$
100		oveq1	$⊢ f = k \cdot_{P} a \to f E M = (k \cdot_{P} a) E M$
101	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
102	87 101	syl	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to P \in LMod$
103	2 76 89 77 102 91 79	lmodvscld	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to k \cdot_{P} a \in U$
104		ovexd	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to (k \cdot_{P} a) E M \in V$
105	5 100 103 104	fvmptd3	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to F (k \cdot_{P} a) = (k \cdot_{P} a) E M$
106		oveq1	$⊢ f = k \cdot_{P} b \to f E M = (k \cdot_{P} b) E M$
107	2 76 89 77 102 91 82	lmodvscld	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to k \cdot_{P} b \in U$
108		ovexd	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to (k \cdot_{P} b) E M \in V$
109	5 106 107 108	fvmptd3	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to F (k \cdot_{P} b) = (k \cdot_{P} b) E M$
110	99 105 109	3eqtr4d	$⊢ ((φ \land F (a) = F (b)) \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to F (k \cdot_{P} a) = F (k \cdot_{P} b)$
111	110	an32s	$⊢ ((φ \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \land F (a) = F (b)) \to F (k \cdot_{P} a) = F (k \cdot_{P} b)$
112	111	ex	$⊢ (φ \land (k \in {Base}_{Scalar (P)} \land a \in U \land b \in U)) \to (F (a) = F (b) \to F (k \cdot_{P} a) = F (k \cdot_{P} b))$
113	6 101	syl	$⊢ φ \to P \in LMod$
114	2 13 14 75 76 77 112 113 89	imaslmhm	$⊢ φ \to (F “_{𝑠} P \in LMod \land F \in (P LMHom (F “_{𝑠} P)))$
115	114	simprd	$⊢ φ \to F \in (P LMHom (F “_{𝑠} P))$

Metamath Proof Explorer

Theorem r1plmhm

Proof