r1peuqusdeg1

Description: Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 . (Contributed by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	r1peuqus.p	$⊢ P = {Poly}_{1} (R)$
	r1peuqus.i	$⊢ I = RSpan (P) (\{F\})$
	r1peuqus.t	$⊢ T = P /_{𝑠} (P ~_{QG} I)$
	r1peuqus.q	$⊢ Q = {Base}_{T}$
	r1peuqus.n	$⊢ N = {Unic}_{1p} (R)$
	r1peuqus.d	$⊢ D = \deg_{1} (R)$
	r1peuqus.r	$⊢ φ \to R \in Domn$
	r1peuqus.f	$⊢ φ \to F \in N$
	r1peuqus.z	$⊢ φ \to Z \in Q$
Assertion	r1peuqusdeg1	$⊢ φ \to \exists! q \in Z D (q) < D (F)$

Proof

Step	Hyp	Ref	Expression
1		r1peuqus.p	$⊢ P = {Poly}_{1} (R)$
2		r1peuqus.i	$⊢ I = RSpan (P) (\{F\})$
3		r1peuqus.t	$⊢ T = P /_{𝑠} (P ~_{QG} I)$
4		r1peuqus.q	$⊢ Q = {Base}_{T}$
5		r1peuqus.n	$⊢ N = {Unic}_{1p} (R)$
6		r1peuqus.d	$⊢ D = \deg_{1} (R)$
7		r1peuqus.r	$⊢ φ \to R \in Domn$
8		r1peuqus.f	$⊢ φ \to F \in N$
9		r1peuqus.z	$⊢ φ \to Z \in Q$
10		eqid	$⊢ {Base}_{P} = {Base}_{P}$
11		eqid	$⊢ +_{P} = +_{P}$
12		eqid	$⊢ \cdot_{P} = \cdot_{P}$
13		eqid	$⊢ P ~_{QG} I = P ~_{QG} I$
14	1	ply1domn	$⊢ R \in Domn \to P \in Domn$
15	7 14	syl	$⊢ φ \to P \in Domn$
16		domnring	$⊢ P \in Domn \to P \in Ring$
17	15 16	syl	$⊢ φ \to P \in Ring$
18	1 10 5	uc1pcl	$⊢ F \in N \to F \in {Base}_{P}$
19	8 18	syl	$⊢ φ \to F \in {Base}_{P}$
20	9 4	eleqtrdi	$⊢ φ \to Z \in {Base}_{T}$
21	10 11 12 13 3 2 17 19 20	ellcsrspsn	$⊢ φ \to \exists p \in {Base}_{P} (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})$
22		domnring	$⊢ R \in Domn \to R \in Ring$
23	7 22	syl	$⊢ φ \to R \in Ring$
24	23	adantr	$⊢ (φ \land p \in {Base}_{P}) \to R \in Ring$
25		simpr	$⊢ (φ \land p \in {Base}_{P}) \to p \in {Base}_{P}$
26	8	adantr	$⊢ (φ \land p \in {Base}_{P}) \to F \in N$
27	1 6 10 11 12 5 24 25 26	ply1divalg3	$⊢ (φ \land p \in {Base}_{P}) \to \exists! s \in {Base}_{P} D (p +_{P} (s \cdot_{P} F)) < D (F)$
28	27	adantr	$⊢ ((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \to \exists! s \in {Base}_{P} D (p +_{P} (s \cdot_{P} F)) < D (F)$
29		ovexd	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to p +_{P} (s \cdot_{P} F) \in V$
30		simpr	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to s \in {Base}_{P}$
31		eqidd	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to p +_{P} (s \cdot_{P} F) = p +_{P} (s \cdot_{P} F)$
32		oveq1	$⊢ y = s \to y \cdot_{P} F = s \cdot_{P} F$
33	32	oveq2d	$⊢ y = s \to p +_{P} (y \cdot_{P} F) = p +_{P} (s \cdot_{P} F)$
34	33	eqeq2d	$⊢ y = s \to (p +_{P} (s \cdot_{P} F) = p +_{P} (y \cdot_{P} F) \leftrightarrow p +_{P} (s \cdot_{P} F) = p +_{P} (s \cdot_{P} F))$
35	34	rspcev	$⊢ (s \in {Base}_{P} \land p +_{P} (s \cdot_{P} F) = p +_{P} (s \cdot_{P} F)) \to \exists y \in {Base}_{P} p +_{P} (s \cdot_{P} F) = p +_{P} (y \cdot_{P} F)$
36	30 31 35	syl2anc	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to \exists y \in {Base}_{P} p +_{P} (s \cdot_{P} F) = p +_{P} (y \cdot_{P} F)$
37		eqeq1	$⊢ z = p +_{P} (s \cdot_{P} F) \to (z = p +_{P} (y \cdot_{P} F) \leftrightarrow p +_{P} (s \cdot_{P} F) = p +_{P} (y \cdot_{P} F))$
38	37	rexbidv	$⊢ z = p +_{P} (s \cdot_{P} F) \to (\exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F) \leftrightarrow \exists y \in {Base}_{P} p +_{P} (s \cdot_{P} F) = p +_{P} (y \cdot_{P} F))$
39	29 36 38	elabd	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to p +_{P} (s \cdot_{P} F) \in \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}$
40		simplrr	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}$
41	39 40	eleqtrrd	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land s \in {Base}_{P}) \to p +_{P} (s \cdot_{P} F) \in Z$
42		simprr	$⊢ ((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \to Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}$
43	42	eqimssd	$⊢ ((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \to Z \subseteq \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}$
44	43	sselda	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land q \in Z) \to q \in \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}$
45		eqeq1	$⊢ z = q \to (z = p +_{P} (y \cdot_{P} F) \leftrightarrow q = p +_{P} (y \cdot_{P} F))$
46	45	rexbidv	$⊢ z = q \to (\exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F) \leftrightarrow \exists y \in {Base}_{P} q = p +_{P} (y \cdot_{P} F))$
47	33	eqeq2d	$⊢ y = s \to (q = p +_{P} (y \cdot_{P} F) \leftrightarrow q = p +_{P} (s \cdot_{P} F))$
48	47	cbvrexvw	$⊢ \exists y \in {Base}_{P} q = p +_{P} (y \cdot_{P} F) \leftrightarrow \exists s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F)$
49	46 48	bitrdi	$⊢ z = q \to (\exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F) \leftrightarrow \exists s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F))$
50	49	elabg	$⊢ q \in \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\} \to (q \in \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\} \leftrightarrow \exists s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F))$
51	50	ibi	$⊢ q \in \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\} \to \exists s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F)$
52	44 51	syl	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land q \in Z) \to \exists s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F)$
53		eqtr2	$⊢ (q = p +_{P} (s \cdot_{P} F) \land q = p +_{P} (t \cdot_{P} F)) \to p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F)$
54	17	ringgrpd	$⊢ φ \to P \in Grp$
55	54	adantr	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to P \in Grp$
56	17	adantr	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to P \in Ring$
57		simpr2	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to s \in {Base}_{P}$
58	19	adantr	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to F \in {Base}_{P}$
59	10 12 56 57 58	ringcld	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to s \cdot_{P} F \in {Base}_{P}$
60		simpr3	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to t \in {Base}_{P}$
61	10 12 56 60 58	ringcld	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to t \cdot_{P} F \in {Base}_{P}$
62		simpr1	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to p \in {Base}_{P}$
63	10 11	grplcan	$⊢ (P \in Grp \land (s \cdot_{P} F \in {Base}_{P} \land t \cdot_{P} F \in {Base}_{P} \land p \in {Base}_{P})) \to (p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F) \leftrightarrow s \cdot_{P} F = t \cdot_{P} F)$
64	55 59 61 62 63	syl13anc	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to (p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F) \leftrightarrow s \cdot_{P} F = t \cdot_{P} F)$
65		eqid	$⊢ 0_{P} = 0_{P}$
66		simplr2	$⊢ ((φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \land s \cdot_{P} F = t \cdot_{P} F) \to s \in {Base}_{P}$
67		simplr3	$⊢ ((φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \land s \cdot_{P} F = t \cdot_{P} F) \to t \in {Base}_{P}$
68	1 65 5	uc1pn0	$⊢ F \in N \to F \neq 0_{P}$
69	8 68	syl	$⊢ φ \to F \neq 0_{P}$
70	19 69	eldifsnd	$⊢ φ \to F \in ({Base}_{P} ∖ \{0_{P}\})$
71	70	ad2antrr	$⊢ ((φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \land s \cdot_{P} F = t \cdot_{P} F) \to F \in ({Base}_{P} ∖ \{0_{P}\})$
72	15	ad2antrr	$⊢ ((φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \land s \cdot_{P} F = t \cdot_{P} F) \to P \in Domn$
73		simpr	$⊢ ((φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \land s \cdot_{P} F = t \cdot_{P} F) \to s \cdot_{P} F = t \cdot_{P} F$
74	10 65 12 66 67 71 72 73	domnrcan	$⊢ ((φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \land s \cdot_{P} F = t \cdot_{P} F) \to s = t$
75	74	ex	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to (s \cdot_{P} F = t \cdot_{P} F \to s = t)$
76	64 75	sylbid	$⊢ (φ \land (p \in {Base}_{P} \land s \in {Base}_{P} \land t \in {Base}_{P})) \to (p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F) \to s = t)$
77	76	3exp2	$⊢ φ \to (p \in {Base}_{P} \to (s \in {Base}_{P} \to (t \in {Base}_{P} \to (p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F) \to s = t))))$
78	77	imp43	$⊢ ((φ \land p \in {Base}_{P}) \land (s \in {Base}_{P} \land t \in {Base}_{P})) \to (p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F) \to s = t)$
79	53 78	syl5	$⊢ ((φ \land p \in {Base}_{P}) \land (s \in {Base}_{P} \land t \in {Base}_{P})) \to ((q = p +_{P} (s \cdot_{P} F) \land q = p +_{P} (t \cdot_{P} F)) \to s = t)$
80	79	ralrimivva	$⊢ (φ \land p \in {Base}_{P}) \to \forall s \in {Base}_{P} \forall t \in {Base}_{P} ((q = p +_{P} (s \cdot_{P} F) \land q = p +_{P} (t \cdot_{P} F)) \to s = t)$
81		oveq1	$⊢ s = t \to s \cdot_{P} F = t \cdot_{P} F$
82	81	oveq2d	$⊢ s = t \to p +_{P} (s \cdot_{P} F) = p +_{P} (t \cdot_{P} F)$
83	82	eqeq2d	$⊢ s = t \to (q = p +_{P} (s \cdot_{P} F) \leftrightarrow q = p +_{P} (t \cdot_{P} F))$
84	83	rmo4	$⊢ \exists^{*} s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F) \leftrightarrow \forall s \in {Base}_{P} \forall t \in {Base}_{P} ((q = p +_{P} (s \cdot_{P} F) \land q = p +_{P} (t \cdot_{P} F)) \to s = t)$
85	80 84	sylibr	$⊢ (φ \land p \in {Base}_{P}) \to \exists^{*} s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F)$
86	85	ad2antrr	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land q \in Z) \to \exists^{*} s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F)$
87		reu5	$⊢ \exists! s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F) \leftrightarrow (\exists s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F) \land \exists^{*} s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F))$
88	52 86 87	sylanbrc	$⊢ (((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \land q \in Z) \to \exists! s \in {Base}_{P} q = p +_{P} (s \cdot_{P} F)$
89		fveq2	$⊢ q = p +_{P} (s \cdot_{P} F) \to D (q) = D (p +_{P} (s \cdot_{P} F))$
90	89	breq1d	$⊢ q = p +_{P} (s \cdot_{P} F) \to (D (q) < D (F) \leftrightarrow D (p +_{P} (s \cdot_{P} F)) < D (F))$
91	41 88 90	reuxfr1ds	$⊢ ((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \to (\exists! q \in Z D (q) < D (F) \leftrightarrow \exists! s \in {Base}_{P} D (p +_{P} (s \cdot_{P} F)) < D (F))$
92	28 91	mpbird	$⊢ ((φ \land p \in {Base}_{P}) \land (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\})) \to \exists! q \in Z D (q) < D (F)$
93	92	ex	$⊢ (φ \land p \in {Base}_{P}) \to ((Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}) \to \exists! q \in Z D (q) < D (F))$
94	93	reximdva	$⊢ φ \to (\exists p \in {Base}_{P} (Z = [p] (P ~_{QG} I) \land Z = \{z \| \exists y \in {Base}_{P} z = p +_{P} (y \cdot_{P} F)\}) \to \exists p \in {Base}_{P} \exists! q \in Z D (q) < D (F))$
95	21 94	mpd	$⊢ φ \to \exists p \in {Base}_{P} \exists! q \in Z D (q) < D (F)$
96		id	$⊢ \exists! q \in Z D (q) < D (F) \to \exists! q \in Z D (q) < D (F)$
97	96	rexlimivw	$⊢ \exists p \in {Base}_{P} \exists! q \in Z D (q) < D (F) \to \exists! q \in Z D (q) < D (F)$
98	95 97	syl	$⊢ φ \to \exists! q \in Z D (q) < D (F)$

Metamath Proof Explorer

Theorem r1peuqusdeg1

Proof