r1pquslmic

Description: The univariate polynomial remainder ring ( F "s P ) is module isomorphic with the quotient ring. (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$
	r1pquslmic.0	$⊢ \underset{˙}{0} = 0_{P}$
	r1pquslmic.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	r1pquslmic.q	$⊢ Q = P /_{𝑠} (P ~_{QG} K)$
Assertion	r1pquslmic	$⊢ φ \to Q ≃_{𝑚} (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		r1pquslmic.0	$⊢ \underset{˙}{0} = 0_{P}$
9		r1pquslmic.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
10		r1pquslmic.q	$⊢ Q = P /_{𝑠} (P ~_{QG} K)$
11		eqidd	$⊢ φ \to F “_{𝑠} P = F “_{𝑠} P$
12	2	a1i	$⊢ φ \to U = {Base}_{P}$
13		eqid	$⊢ +_{P} = +_{P}$
14	6	adantr	$⊢ (φ \land f \in U) \to R \in Ring$
15		simpr	$⊢ (φ \land f \in U) \to f \in U$
16	7	adantr	$⊢ (φ \land f \in U) \to M \in N$
17	3 1 2 4	r1pcl	$⊢ (R \in Ring \land f \in U \land M \in N) \to f E M \in U$
18	14 15 16 17	syl3anc	$⊢ (φ \land f \in U) \to f E M \in U$
19	18 5	fmptd	$⊢ φ \to F : U ⟶ U$
20		fimadmfo	$⊢ F : U ⟶ U \to F : U \underset{onto}{⟶} F [U]$
21	19 20	syl	$⊢ φ \to F : U \underset{onto}{⟶} F [U]$
22		anass	$⊢ ((φ \land a \in U) \land b \in U) \leftrightarrow (φ \land (a \in U \land b \in U))$
23		simplr	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F (a) = F (f)$
24		simpr	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F (b) = F (q)$
25	23 24	oveq12d	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F (a) +_{(F “_{𝑠} P)} F (b) = F (f) +_{(F “_{𝑠} P)} F (q)$
26	1 2 3 4 5 6 7	r1plmhm	$⊢ φ \to F \in (P LMHom (F “_{𝑠} P))$
27	26	lmhmghmd	$⊢ φ \to F \in (P GrpHom (F “_{𝑠} P))$
28	27	ad6antr	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F \in (P GrpHom (F “_{𝑠} P))$
29		simp-6r	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to a \in U$
30		simp-5r	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to b \in U$
31		eqid	$⊢ +_{(F “_{𝑠} P)} = +_{(F “_{𝑠} P)}$
32	2 13 31	ghmlin	$⊢ (F \in (P GrpHom (F “_{𝑠} P)) \land a \in U \land b \in U) \to F (a +_{P} b) = F (a) +_{(F “_{𝑠} P)} F (b)$
33	28 29 30 32	syl3anc	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F (a +_{P} b) = F (a) +_{(F “_{𝑠} P)} F (b)$
34		simp-4r	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to f \in U$
35		simpllr	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to q \in U$
36	2 13 31	ghmlin	$⊢ (F \in (P GrpHom (F “_{𝑠} P)) \land f \in U \land q \in U) \to F (f +_{P} q) = F (f) +_{(F “_{𝑠} P)} F (q)$
37	28 34 35 36	syl3anc	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F (f +_{P} q) = F (f) +_{(F “_{𝑠} P)} F (q)$
38	25 33 37	3eqtr4d	$⊢ ((((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \land F (a) = F (f)) \land F (b) = F (q)) \to F (a +_{P} b) = F (f +_{P} q)$
39	38	expl	$⊢ ((((φ \land a \in U) \land b \in U) \land f \in U) \land q \in U) \to ((F (a) = F (f) \land F (b) = F (q)) \to F (a +_{P} b) = F (f +_{P} q))$
40	39	anasss	$⊢ (((φ \land a \in U) \land b \in U) \land (f \in U \land q \in U)) \to ((F (a) = F (f) \land F (b) = F (q)) \to F (a +_{P} b) = F (f +_{P} q))$
41	22 40	sylanbr	$⊢ ((φ \land (a \in U \land b \in U)) \land (f \in U \land q \in U)) \to ((F (a) = F (f) \land F (b) = F (q)) \to F (a +_{P} b) = F (f +_{P} q))$
42	41	3impa	$⊢ (φ \land (a \in U \land b \in U) \land (f \in U \land q \in U)) \to ((F (a) = F (f) \land F (b) = F (q)) \to F (a +_{P} b) = F (f +_{P} q))$
43	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
44	6 43	syl	$⊢ φ \to P \in Ring$
45	44	ringgrpd	$⊢ φ \to P \in Grp$
46	45	grpmndd	$⊢ φ \to P \in Mnd$
47	11 12 13 21 42 46 8	imasmnd	$⊢ φ \to (F “_{𝑠} P \in Mnd \land F (\underset{˙}{0}) = 0_{(F “_{𝑠} P)})$
48	47	simprd	$⊢ φ \to F (\underset{˙}{0}) = 0_{(F “_{𝑠} P)}$
49		oveq1	$⊢ f = \underset{˙}{0} \to f E M = \underset{˙}{0} E M$
50	1 2 4 3 6 7 8	r1p0	$⊢ φ \to \underset{˙}{0} E M = \underset{˙}{0}$
51	49 50	sylan9eqr	$⊢ (φ \land f = \underset{˙}{0}) \to f E M = \underset{˙}{0}$
52	2 8	ring0cl	$⊢ P \in Ring \to \underset{˙}{0} \in U$
53	44 52	syl	$⊢ φ \to \underset{˙}{0} \in U$
54	5 51 53 53	fvmptd2	$⊢ φ \to F (\underset{˙}{0}) = \underset{˙}{0}$
55	48 54	eqtr3d	$⊢ φ \to 0_{(F “_{𝑠} P)} = \underset{˙}{0}$
56	55	sneqd	$⊢ φ \to \{0_{(F “_{𝑠} P)}\} = \{\underset{˙}{0}\}$
57	56	imaeq2d	$⊢ φ \to F^{-1} [\{0_{(F “_{𝑠} P)}\}] = F^{-1} [\{\underset{˙}{0}\}]$
58	57 9	eqtr4di	$⊢ φ \to F^{-1} [\{0_{(F “_{𝑠} P)}\}] = K$
59	58	oveq2d	$⊢ φ \to P ~_{QG} F^{-1} [\{0_{(F “_{𝑠} P)}\}] = P ~_{QG} K$
60	59	oveq2d	$⊢ φ \to P /_{𝑠} (P ~_{QG} F^{-1} [\{0_{(F “_{𝑠} P)}\}]) = P /_{𝑠} (P ~_{QG} K)$
61	60 10	eqtr4di	$⊢ φ \to P /_{𝑠} (P ~_{QG} F^{-1} [\{0_{(F “_{𝑠} P)}\}]) = Q$
62		eqid	$⊢ 0_{(F “_{𝑠} P)} = 0_{(F “_{𝑠} P)}$
63		eqid	$⊢ F^{-1} [\{0_{(F “_{𝑠} P)}\}] = F^{-1} [\{0_{(F “_{𝑠} P)}\}]$
64		eqid	$⊢ P /_{𝑠} (P ~_{QG} F^{-1} [\{0_{(F “_{𝑠} P)}\}]) = P /_{𝑠} (P ~_{QG} F^{-1} [\{0_{(F “_{𝑠} P)}\}])$
65	19	ffnd	$⊢ φ \to F Fn U$
66		fnima	$⊢ F Fn U \to F [U] = ran F$
67	65 66	syl	$⊢ φ \to F [U] = ran F$
68	1	fvexi	$⊢ P \in V$
69	68	a1i	$⊢ φ \to P \in V$
70	11 12 21 69	imasbas	$⊢ φ \to F [U] = {Base}_{(F “_{𝑠} P)}$
71	67 70	eqtr3d	$⊢ φ \to ran F = {Base}_{(F “_{𝑠} P)}$
72	62 26 63 64 71	lmicqusker	$⊢ φ \to (P /_{𝑠} (P ~_{QG} F^{-1} [\{0_{(F “_{𝑠} P)}\}])) ≃_{𝑚} (F “_{𝑠} P)$
73	61 72	eqbrtrrd	$⊢ φ \to Q ≃_{𝑚} (F “_{𝑠} P)$

Metamath Proof Explorer

Theorem r1pquslmic

Proof