Theorem ply1divmo

Description: Uniqueness of a quotient in a polynomial division. For polynomials F , G such that G =/= 0 and the leading coefficient of G is not a zero divisor, there is at most one polynomial q which satisfies F = ( G x. q ) + r where the degree of r is less than the degree of G . (Contributed by Stefan O'Rear, 26-Mar-2015) (Revised by NM, 17-Jun-2017)

	Ref	Expression
Hypotheses	ply1divalg.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1divalg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	ply1divalg.b	$$⊢B={\mathrm{Base}}_P$$
	ply1divalg.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	ply1divalg.z	$$⊢\underset{\dot{}}{0}=0_P$$
	ply1divalg.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	ply1divalg.r1	$$⊢\phi \to R\in \mathrm{Ring}$$
	ply1divalg.f	$$⊢\phi \to F\in B$$
	ply1divalg.g1	$$⊢\phi \to G\in B$$
	ply1divalg.g2	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
	ply1divmo.g3	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in E$$
	ply1divmo.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
Assertion	ply1divmo	$$⊢\phi \to {\exists }^{*}q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1divalg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		ply1divalg.b	$$⊢B={\mathrm{Base}}_P$$
4		ply1divalg.m	$$⊢\underset{\dot{}}{-}={-}_P$$
5		ply1divalg.z	$$⊢\underset{\dot{}}{0}=0_P$$
6		ply1divalg.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
7		ply1divalg.r1	$$⊢\phi \to R\in \mathrm{Ring}$$
8		ply1divalg.f	$$⊢\phi \to F\in B$$
9		ply1divalg.g1	$$⊢\phi \to G\in B$$
10		ply1divalg.g2	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
11		ply1divmo.g3	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in E$$
12		ply1divmo.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
13	7	adantr	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to R\in \mathrm{Ring}$$
14	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
15	13 14	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to P\in \mathrm{Ring}$$
16		ringgrp	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{Grp}$$
17	15 16	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to P\in \mathrm{Grp}$$
18	8	adantr	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to F\in B$$
19	9	adantr	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to G\in B$$
20		simprl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to q\in B$$
21	3 6	ringcl	$$⊢\left(P\in \mathrm{Ring}\wedge G\in B\wedge q\in B\right)\to G\underset{\dot{}}{\bullet }q\in B$$
22	15 19 20 21	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to G\underset{\dot{}}{\bullet }q\in B$$
23	3 4	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge F\in B\wedge G\underset{\dot{}}{\bullet }q\in B\right)\to F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\in B$$
24	17 18 22 23	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\in B$$
25		simprr	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to r\in B$$
26	3 6	ringcl	$$⊢\left(P\in \mathrm{Ring}\wedge G\in B\wedge r\in B\right)\to G\underset{\dot{}}{\bullet }r\in B$$
27	15 19 25 26	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to G\underset{\dot{}}{\bullet }r\in B$$
28	3 4	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge F\in B\wedge G\underset{\dot{}}{\bullet }r\in B\right)\to F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\in B$$
29	17 18 27 28	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\in B$$
30	3 4	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\in B\wedge F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\in B\right)\to \left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\in B$$
31	17 24 29 30	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\in B$$
32	2 1 3	deg1xrcl	$$⊢\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\in B\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\in {ℝ}^{*}$$
33	31 32	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\in {ℝ}^{*}$$
34	2 1 3	deg1xrcl	$$⊢F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\in B\to D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\in {ℝ}^{*}$$
35	29 34	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\in {ℝ}^{*}$$
36	2 1 3	deg1xrcl	$$⊢F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\in B\to D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\in {ℝ}^{*}$$
37	24 36	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\in {ℝ}^{*}$$
38	35 37	ifcld	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)\in {ℝ}^{*}$$
39	2 1 3	deg1xrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
40	19 39	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to D\left(G\right)\in {ℝ}^{*}$$
41	33 38 40	3jca	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\in {ℝ}^{*}\wedge if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\right)$$
42	41	adantr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)\to \left(D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\in {ℝ}^{*}\wedge if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\right)$$
43	1 2 13 3 4 24 29	deg1suble	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\le if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)$$
44	43	adantr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\le if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)$$
45		xrmaxlt	$$⊢\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\in {ℝ}^{*}\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\right)\to \left(if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)<D\left(G\right)\leftrightarrow \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)$$
46	37 35 40 45	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)<D\left(G\right)\leftrightarrow \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)$$
47	46	biimpar	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)\to if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)<D\left(G\right)$$
48	44 47	jca	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)\to \left(D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\le if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)\wedge if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)<D\left(G\right)\right)$$
49		xrlelttr	$$⊢\left(D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\in {ℝ}^{*}\wedge if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\right)\to \left(\left(D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\le if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)\wedge if\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\le D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right),D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\right)<D\left(G\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)\right)$$
50	42 48 49	sylc	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)$$
51	50	ex	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)\right)$$
52	2 1 5 3	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\wedge G\ne \underset{\dot{}}{0}\right)\to D\left(G\right)\in {\mathbb{N}}_0$$
53	7 9 10 52	syl3anc	$$⊢\phi \to D\left(G\right)\in {\mathbb{N}}_0$$
54	53	ad2antrr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(G\right)\in {\mathbb{N}}_0$$
55	54	nn0red	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(G\right)\in ℝ$$
56	7	ad2antrr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to R\in \mathrm{Ring}$$
57	3 4	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge r\in B\wedge q\in B\right)\to r\underset{\dot{}}{-}q\in B$$
58	17 25 20 57	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to r\underset{\dot{}}{-}q\in B$$
59	58	adantr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to r\underset{\dot{}}{-}q\in B$$
60	3 5 4	grpsubeq0	$$⊢\left(P\in \mathrm{Grp}\wedge r\in B\wedge q\in B\right)\to \left(r\underset{\dot{}}{-}q=\underset{\dot{}}{0}\leftrightarrow r=q\right)$$
61	17 25 20 60	syl3anc	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(r\underset{\dot{}}{-}q=\underset{\dot{}}{0}\leftrightarrow r=q\right)$$
62		equcom	$$⊢r=q\leftrightarrow q=r$$
63	61 62	bitrdi	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(r\underset{\dot{}}{-}q=\underset{\dot{}}{0}\leftrightarrow q=r\right)$$
64	63	necon3bid	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(r\underset{\dot{}}{-}q\ne \underset{\dot{}}{0}\leftrightarrow q\ne r\right)$$
65	64	biimpar	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to r\underset{\dot{}}{-}q\ne \underset{\dot{}}{0}$$
66	2 1 5 3	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge r\underset{\dot{}}{-}q\in B\wedge r\underset{\dot{}}{-}q\ne \underset{\dot{}}{0}\right)\to D\left(r\underset{\dot{}}{-}q\right)\in {\mathbb{N}}_0$$
67	56 59 65 66	syl3anc	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(r\underset{\dot{}}{-}q\right)\in {\mathbb{N}}_0$$
68		nn0addge1	$$⊢\left(D\left(G\right)\in ℝ\wedge D\left(r\underset{\dot{}}{-}q\right)\in {\mathbb{N}}_0\right)\to D\left(G\right)\le D\left(G\right)+D\left(r\underset{\dot{}}{-}q\right)$$
69	55 67 68	syl2anc	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(G\right)\le D\left(G\right)+D\left(r\underset{\dot{}}{-}q\right)$$
70	9	ad2antrr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to G\in B$$
71	10	ad2antrr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to G\ne \underset{\dot{}}{0}$$
72	11	ad2antrr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in E$$
73	2 1 12 3 6 5 56 70 71 72 59 65	deg1mul2	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(G\underset{\dot{}}{\bullet }\left(r\underset{\dot{}}{-}q\right)\right)=D\left(G\right)+D\left(r\underset{\dot{}}{-}q\right)$$
74	69 73	breqtrrd	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(G\right)\le D\left(G\underset{\dot{}}{\bullet }\left(r\underset{\dot{}}{-}q\right)\right)$$
75		ringabl	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{Abel}$$
76	15 75	syl	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to P\in \mathrm{Abel}$$
77	3 4 76 18 22 27	ablnnncan1	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)=\left(G\underset{\dot{}}{\bullet }r\right)\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)$$
78	3 6 4 15 19 25 20	ringsubdi	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to G\underset{\dot{}}{\bullet }\left(r\underset{\dot{}}{-}q\right)=\left(G\underset{\dot{}}{\bullet }r\right)\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)$$
79	77 78	eqtr4d	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)=G\underset{\dot{}}{\bullet }\left(r\underset{\dot{}}{-}q\right)$$
80	79	fveq2d	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)=D\left(G\underset{\dot{}}{\bullet }\left(r\underset{\dot{}}{-}q\right)\right)$$
81	80	adantr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)=D\left(G\underset{\dot{}}{\bullet }\left(r\underset{\dot{}}{-}q\right)\right)$$
82	74 81	breqtrrd	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to D\left(G\right)\le D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)$$
83	40 33	xrlenltd	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(D\left(G\right)\le D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\leftrightarrow \neg D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)\right)$$
84	83	adantr	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to \left(D\left(G\right)\le D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)\leftrightarrow \neg D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)\right)$$
85	82 84	mpbid	$$⊢\left(\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\wedge q\ne r\right)\to \neg D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)$$
86	85	ex	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(q\ne r\to \neg D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)\right)$$
87	86	necon4ad	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(D\left(\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)\underset{\dot{}}{-}\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)\right)<D\left(G\right)\to q=r\right)$$
88	51 87	syld	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\to q=r\right)$$
89	88	ralrimivva	$$⊢\phi \to \forall q\in B\forall r\in B\left(\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\to q=r\right)$$
90		oveq2	$$⊢q=r\to G\underset{\dot{}}{\bullet }q=G\underset{\dot{}}{\bullet }r$$
91	90	oveq2d	$$⊢q=r\to F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)=F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)$$
92	91	fveq2d	$$⊢q=r\to D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)=D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)$$
93	92	breq1d	$$⊢q=r\to \left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\leftrightarrow D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)$$
94	93	rmo4	$$⊢{\exists }^{*}q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\leftrightarrow \forall q\in B\forall r\in B\left(\left(D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge D\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }r\right)\right)<D\left(G\right)\right)\to q=r\right)$$
95	89 94	sylibr	$$⊢\phi \to {\exists }^{*}q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)$$