Theorem ply1divalg3

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

	Ref	Expression
Hypotheses	ply1divalg3.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1divalg3.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	ply1divalg3.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1divalg3.m	⊢ + = ( +g ‘ 𝑃 )
	ply1divalg3.t	⊢ ∙ = ( .r ‘ 𝑃 )
	ply1divalg3.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
	ply1divalg3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1divalg3.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	ply1divalg3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
Assertion	ply1divalg3	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1divalg3.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1divalg3.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		ply1divalg3.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1divalg3.m	⊢ + = ( +g ‘ 𝑃 )
5		ply1divalg3.t	⊢ ∙ = ( .r ‘ 𝑃 )
6		ply1divalg3.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
7		ply1divalg3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		ply1divalg3.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		ply1divalg3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
10		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
11		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
12	1 3 6	uc1pcl	⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵 )
13	9 12	syl	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
14	1 11 6	uc1pn0	⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
15	9 14	syl	⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
16		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
17	2 16 6	uc1pldg	⊢ ( 𝐺 ∈ 𝐶 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Unit ‘ 𝑅 ) )
18	9 17	syl	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Unit ‘ 𝑅 ) )
19	1 2 3 10 11 5 7 8 13 15 18 16	ply1divalg2	⊢ ( 𝜑 → ∃! 𝑝 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑝 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
20		eqid	⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
21	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
22	7 21	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
23	22	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑃 ∈ Grp )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑞 ∈ 𝐵 )
26	3 20 24 25	grpinvcld	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∈ 𝐵 )
27	3 20 23	grpinvf1o	⊢ ( 𝜑 → ( invg ‘ 𝑃 ) : 𝐵 –1-1-onto→ 𝐵 )
28		f1ofveu	⊢ ( ( ( invg ‘ 𝑃 ) : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ∃! 𝑞 ∈ 𝐵 ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) = 𝑝 )
29	27 28	sylan	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ∃! 𝑞 ∈ 𝐵 ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) = 𝑝 )
30		eqcom	⊢ ( 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ↔ ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) = 𝑝 )
31	30	reubii	⊢ ( ∃! 𝑞 ∈ 𝐵 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ↔ ∃! 𝑞 ∈ 𝐵 ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) = 𝑝 )
32	29 31	sylibr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ∃! 𝑞 ∈ 𝐵 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) )
33		oveq1	⊢ ( 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) → ( 𝑝 ∙ 𝐺 ) = ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) )
34	33	oveq2d	⊢ ( 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑝 ∙ 𝐺 ) ) = ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) )
35	34	fveq2d	⊢ ( 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) → ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑝 ∙ 𝐺 ) ) ) = ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) )
36	35	breq1d	⊢ ( 𝑝 = ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) → ( ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑝 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
37	26 32 36	reuxfr1ds	⊢ ( 𝜑 → ( ∃! 𝑝 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑝 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
38	19 37	mpbid	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
39	22	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑃 ∈ Ring )
40	13	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
41	3 5 39 26 40	ringcld	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ∈ 𝐵 )
42	3 4 20 10	grpsubval	⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ∈ 𝐵 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) = ( 𝐹 + ( ( invg ‘ 𝑃 ) ‘ ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) )
43	8 41 42	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) = ( 𝐹 + ( ( invg ‘ 𝑃 ) ‘ ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) )
44	3 5 20 39 25 40	ringmneg1	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) = ( ( invg ‘ 𝑃 ) ‘ ( 𝑞 ∙ 𝐺 ) ) )
45	44	fveq2d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( invg ‘ 𝑃 ) ‘ ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) = ( ( invg ‘ 𝑃 ) ‘ ( ( invg ‘ 𝑃 ) ‘ ( 𝑞 ∙ 𝐺 ) ) ) )
46	3 5 39 25 40	ringcld	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑞 ∙ 𝐺 ) ∈ 𝐵 )
47	3 20	grpinvinv	⊢ ( ( 𝑃 ∈ Grp ∧ ( 𝑞 ∙ 𝐺 ) ∈ 𝐵 ) → ( ( invg ‘ 𝑃 ) ‘ ( ( invg ‘ 𝑃 ) ‘ ( 𝑞 ∙ 𝐺 ) ) ) = ( 𝑞 ∙ 𝐺 ) )
48	23 46 47	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( invg ‘ 𝑃 ) ‘ ( ( invg ‘ 𝑃 ) ‘ ( 𝑞 ∙ 𝐺 ) ) ) = ( 𝑞 ∙ 𝐺 ) )
49	45 48	eqtrd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( invg ‘ 𝑃 ) ‘ ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) = ( 𝑞 ∙ 𝐺 ) )
50	49	oveq2d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 + ( ( invg ‘ 𝑃 ) ‘ ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) = ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) )
51	43 50	eqtrd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) = ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) )
52	51	fveq2d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) = ( 𝐷 ‘ ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) ) )
53	52	breq1d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
54	53	reubidva	⊢ ( 𝜑 → ( ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( ( ( invg ‘ 𝑃 ) ‘ 𝑞 ) ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
55	38 54	mpbid	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 + ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )