ply1divalg3

Description: Uniqueness of polynomial remainder: convert the subtraction in ply1divalg2 to addition. (Contributed by SN, 20-Jun-2025)

	Ref	Expression
Hypotheses	ply1divalg3.p	$⊢ P = {Poly}_{1} (R)$
	ply1divalg3.d	$⊢ D = \deg_{1} (R)$
	ply1divalg3.b	$⊢ B = {Base}_{P}$
	ply1divalg3.m	$⊢ \underset{˙}{+} = +_{P}$
	ply1divalg3.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	ply1divalg3.c	$⊢ C = {Unic}_{1p} (R)$
	ply1divalg3.r	$⊢ φ \to R \in Ring$
	ply1divalg3.f	$⊢ φ \to F \in B$
	ply1divalg3.g	$⊢ φ \to G \in C$
Assertion	ply1divalg3	$⊢ φ \to \exists! q \in B D (F \underset{˙}{+} (q \underset{˙}{∙} G)) < D (G)$

Proof

Step	Hyp	Ref	Expression
1		ply1divalg3.p	$⊢ P = {Poly}_{1} (R)$
2		ply1divalg3.d	$⊢ D = \deg_{1} (R)$
3		ply1divalg3.b	$⊢ B = {Base}_{P}$
4		ply1divalg3.m	$⊢ \underset{˙}{+} = +_{P}$
5		ply1divalg3.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
6		ply1divalg3.c	$⊢ C = {Unic}_{1p} (R)$
7		ply1divalg3.r	$⊢ φ \to R \in Ring$
8		ply1divalg3.f	$⊢ φ \to F \in B$
9		ply1divalg3.g	$⊢ φ \to G \in C$
10		eqid	$⊢ -_{P} = -_{P}$
11		eqid	$⊢ 0_{P} = 0_{P}$
12	1 3 6	uc1pcl	$⊢ G \in C \to G \in B$
13	9 12	syl	$⊢ φ \to G \in B$
14	1 11 6	uc1pn0	$⊢ G \in C \to G \neq 0_{P}$
15	9 14	syl	$⊢ φ \to G \neq 0_{P}$
16		eqid	$⊢ Unit (R) = Unit (R)$
17	2 16 6	uc1pldg	$⊢ G \in C \to {coe}_{1} (G) (D (G)) \in Unit (R)$
18	9 17	syl	$⊢ φ \to {coe}_{1} (G) (D (G)) \in Unit (R)$
19	1 2 3 10 11 5 7 8 13 15 18 16	ply1divalg2	$⊢ φ \to \exists! p \in B D (F -_{P} (p \underset{˙}{∙} G)) < D (G)$
20		eqid	$⊢ {inv}_{g} (P) = {inv}_{g} (P)$
21	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
22	7 21	syl	$⊢ φ \to P \in Ring$
23	22	ringgrpd	$⊢ φ \to P \in Grp$
24	23	adantr	$⊢ (φ \land q \in B) \to P \in Grp$
25		simpr	$⊢ (φ \land q \in B) \to q \in B$
26	3 20 24 25	grpinvcld	$⊢ (φ \land q \in B) \to {inv}_{g} (P) (q) \in B$
27	3 20 23	grpinvf1o	$⊢ φ \to {inv}_{g} (P) : B \underset{1-1 onto}{⟶} B$
28		f1ofveu	$⊢ ({inv}_{g} (P) : B \underset{1-1 onto}{⟶} B \land p \in B) \to \exists! q \in B {inv}_{g} (P) (q) = p$
29	27 28	sylan	$⊢ (φ \land p \in B) \to \exists! q \in B {inv}_{g} (P) (q) = p$
30		eqcom	$⊢ p = {inv}_{g} (P) (q) \leftrightarrow {inv}_{g} (P) (q) = p$
31	30	reubii	$⊢ \exists! q \in B p = {inv}_{g} (P) (q) \leftrightarrow \exists! q \in B {inv}_{g} (P) (q) = p$
32	29 31	sylibr	$⊢ (φ \land p \in B) \to \exists! q \in B p = {inv}_{g} (P) (q)$
33		oveq1	$⊢ p = {inv}_{g} (P) (q) \to p \underset{˙}{∙} G = {inv}_{g} (P) (q) \underset{˙}{∙} G$
34	33	oveq2d	$⊢ p = {inv}_{g} (P) (q) \to F -_{P} (p \underset{˙}{∙} G) = F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)$
35	34	fveq2d	$⊢ p = {inv}_{g} (P) (q) \to D (F -_{P} (p \underset{˙}{∙} G)) = D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G))$
36	35	breq1d	$⊢ p = {inv}_{g} (P) (q) \to (D (F -_{P} (p \underset{˙}{∙} G)) < D (G) \leftrightarrow D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)) < D (G))$
37	26 32 36	reuxfr1ds	$⊢ φ \to (\exists! p \in B D (F -_{P} (p \underset{˙}{∙} G)) < D (G) \leftrightarrow \exists! q \in B D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)) < D (G))$
38	19 37	mpbid	$⊢ φ \to \exists! q \in B D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)) < D (G)$
39	22	adantr	$⊢ (φ \land q \in B) \to P \in Ring$
40	13	adantr	$⊢ (φ \land q \in B) \to G \in B$
41	3 5 39 26 40	ringcld	$⊢ (φ \land q \in B) \to {inv}_{g} (P) (q) \underset{˙}{∙} G \in B$
42	3 4 20 10	grpsubval	$⊢ (F \in B \land {inv}_{g} (P) (q) \underset{˙}{∙} G \in B) \to F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G) = F \underset{˙}{+} {inv}_{g} (P) ({inv}_{g} (P) (q) \underset{˙}{∙} G)$
43	8 41 42	syl2an2r	$⊢ (φ \land q \in B) \to F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G) = F \underset{˙}{+} {inv}_{g} (P) ({inv}_{g} (P) (q) \underset{˙}{∙} G)$
44	3 5 20 39 25 40	ringmneg1	$⊢ (φ \land q \in B) \to {inv}_{g} (P) (q) \underset{˙}{∙} G = {inv}_{g} (P) (q \underset{˙}{∙} G)$
45	44	fveq2d	$⊢ (φ \land q \in B) \to {inv}_{g} (P) ({inv}_{g} (P) (q) \underset{˙}{∙} G) = {inv}_{g} (P) ({inv}_{g} (P) (q \underset{˙}{∙} G))$
46	3 5 39 25 40	ringcld	$⊢ (φ \land q \in B) \to q \underset{˙}{∙} G \in B$
47	3 20	grpinvinv	$⊢ (P \in Grp \land q \underset{˙}{∙} G \in B) \to {inv}_{g} (P) ({inv}_{g} (P) (q \underset{˙}{∙} G)) = q \underset{˙}{∙} G$
48	23 46 47	syl2an2r	$⊢ (φ \land q \in B) \to {inv}_{g} (P) ({inv}_{g} (P) (q \underset{˙}{∙} G)) = q \underset{˙}{∙} G$
49	45 48	eqtrd	$⊢ (φ \land q \in B) \to {inv}_{g} (P) ({inv}_{g} (P) (q) \underset{˙}{∙} G) = q \underset{˙}{∙} G$
50	49	oveq2d	$⊢ (φ \land q \in B) \to F \underset{˙}{+} {inv}_{g} (P) ({inv}_{g} (P) (q) \underset{˙}{∙} G) = F \underset{˙}{+} (q \underset{˙}{∙} G)$
51	43 50	eqtrd	$⊢ (φ \land q \in B) \to F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G) = F \underset{˙}{+} (q \underset{˙}{∙} G)$
52	51	fveq2d	$⊢ (φ \land q \in B) \to D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)) = D (F \underset{˙}{+} (q \underset{˙}{∙} G))$
53	52	breq1d	$⊢ (φ \land q \in B) \to (D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)) < D (G) \leftrightarrow D (F \underset{˙}{+} (q \underset{˙}{∙} G)) < D (G))$
54	53	reubidva	$⊢ φ \to (\exists! q \in B D (F -_{P} ({inv}_{g} (P) (q) \underset{˙}{∙} G)) < D (G) \leftrightarrow \exists! q \in B D (F \underset{˙}{+} (q \underset{˙}{∙} G)) < D (G))$
55	38 54	mpbid	$⊢ φ \to \exists! q \in B D (F \underset{˙}{+} (q \underset{˙}{∙} G)) < D (G)$

Metamath Proof Explorer

Theorem ply1divalg3

Proof