Metamath Proof Explorer

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 = ( Poly1 ` R )
ply1divalg.d 
|- D = ( deg1 ` R )
ply1divalg.b 
|- B = ( Base ` P )
ply1divalg.m 
|- .- = ( -g ` P )
ply1divalg.z 
|- .0. = ( 0g ` P )
ply1divalg.t 
|- .xb = ( .r ` P )
ply1divalg.r1 
|- ( ph -> R e. Ring )
ply1divalg.f 
|- ( ph -> F e. B )
ply1divalg.g1 
|- ( ph -> G e. B )
ply1divalg.g2 
|- ( ph -> G =/= .0. )
ply1divmo.g3 
|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. E )
ply1divmo.e 
|- E = ( RLReg ` R )
Assertion ply1divmo 
|- ( ph -> E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )

Proof

Step Hyp Ref Expression
1 ply1divalg.p 
 |-  P = ( Poly1 ` R )
2 ply1divalg.d 
 |-  D = ( deg1 ` R )
3 ply1divalg.b 
 |-  B = ( Base ` P )
4 ply1divalg.m 
 |-  .- = ( -g ` P )
5 ply1divalg.z 
 |-  .0. = ( 0g ` P )
6 ply1divalg.t 
 |-  .xb = ( .r ` P )
7 ply1divalg.r1 
 |-  ( ph -> R e. Ring )
8 ply1divalg.f 
 |-  ( ph -> F e. B )
9 ply1divalg.g1 
 |-  ( ph -> G e. B )
10 ply1divalg.g2 
 |-  ( ph -> G =/= .0. )
11 ply1divmo.g3 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. E )
12 ply1divmo.e 
 |-  E = ( RLReg ` R )
13 7 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> R e. Ring )
14 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 13 14 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> P e. Ring )
16 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
17 15 16 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> P e. Grp )
18 8 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> F e. B )
19 9 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> G e. B )
20 simprl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> q e. B )
21 3 6 ringcl 
 |-  ( ( P e. Ring /\ G e. B /\ q e. B ) -> ( G .xb q ) e. B )
22 15 19 20 21 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( G .xb q ) e. B )
23 3 4 grpsubcl 
 |-  ( ( P e. Grp /\ F e. B /\ ( G .xb q ) e. B ) -> ( F .- ( G .xb q ) ) e. B )
24 17 18 22 23 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F .- ( G .xb q ) ) e. B )
25 simprr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> r e. B )
26 3 6 ringcl 
 |-  ( ( P e. Ring /\ G e. B /\ r e. B ) -> ( G .xb r ) e. B )
27 15 19 25 26 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( G .xb r ) e. B )
28 3 4 grpsubcl 
 |-  ( ( P e. Grp /\ F e. B /\ ( G .xb r ) e. B ) -> ( F .- ( G .xb r ) ) e. B )
29 17 18 27 28 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F .- ( G .xb r ) ) e. B )
30 3 4 grpsubcl 
 |-  ( ( P e. Grp /\ ( F .- ( G .xb q ) ) e. B /\ ( F .- ( G .xb r ) ) e. B ) -> ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) e. B )
31 17 24 29 30 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) e. B )
32 2 1 3 deg1xrcl 
 |-  ( ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) e. B -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) e. RR* )
33 31 32 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) e. RR* )
34 2 1 3 deg1xrcl 
 |-  ( ( F .- ( G .xb r ) ) e. B -> ( D ` ( F .- ( G .xb r ) ) ) e. RR* )
35 29 34 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( D ` ( F .- ( G .xb r ) ) ) e. RR* )
36 2 1 3 deg1xrcl 
 |-  ( ( F .- ( G .xb q ) ) e. B -> ( D ` ( F .- ( G .xb q ) ) ) e. RR* )
37 24 36 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( D ` ( F .- ( G .xb q ) ) ) e. RR* )
38 35 37 ifcld 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) e. RR* )
39 2 1 3 deg1xrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
40 19 39 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( D ` G ) e. RR* )
41 33 38 40 3jca 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) e. RR* /\ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) e. RR* /\ ( D ` G ) e. RR* ) )
42 41 adantr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) -> ( ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) e. RR* /\ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) e. RR* /\ ( D ` G ) e. RR* ) )
43 1 2 13 3 4 24 29 deg1suble 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) <_ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) )
44 43 adantr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) <_ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) )
45 xrmaxlt 
 |-  ( ( ( D ` ( F .- ( G .xb q ) ) ) e. RR* /\ ( D ` ( F .- ( G .xb r ) ) ) e. RR* /\ ( D ` G ) e. RR* ) -> ( if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) < ( D ` G ) <-> ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) )
46 37 35 40 45 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) < ( D ` G ) <-> ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) )
47 46 biimpar 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) -> if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) < ( D ` G ) )
48 44 47 jca 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) -> ( ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) <_ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) /\ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) < ( D ` G ) ) )
49 xrlelttr 
 |-  ( ( ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) e. RR* /\ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) e. RR* /\ ( D ` G ) e. RR* ) -> ( ( ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) <_ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) /\ if ( ( D ` ( F .- ( G .xb q ) ) ) <_ ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb r ) ) ) , ( D ` ( F .- ( G .xb q ) ) ) ) < ( D ` G ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) ) )
50 42 48 49 sylc 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) )
51 50 ex 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) ) )
52 2 1 5 3 deg1nn0cl 
 |-  ( ( R e. Ring /\ G e. B /\ G =/= .0. ) -> ( D ` G ) e. NN0 )
53 7 9 10 52 syl3anc 
 |-  ( ph -> ( D ` G ) e. NN0 )
54 53 ad2antrr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` G ) e. NN0 )
55 54 nn0red 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` G ) e. RR )
56 7 ad2antrr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> R e. Ring )
57 3 4 grpsubcl 
 |-  ( ( P e. Grp /\ r e. B /\ q e. B ) -> ( r .- q ) e. B )
58 17 25 20 57 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( r .- q ) e. B )
59 58 adantr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( r .- q ) e. B )
60 3 5 4 grpsubeq0 
 |-  ( ( P e. Grp /\ r e. B /\ q e. B ) -> ( ( r .- q ) = .0. <-> r = q ) )
61 17 25 20 60 syl3anc 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( r .- q ) = .0. <-> r = q ) )
62 equcom 
 |-  ( r = q <-> q = r )
63 61 62 bitrdi 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( r .- q ) = .0. <-> q = r ) )
64 63 necon3bid 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( r .- q ) =/= .0. <-> q =/= r ) )
65 64 biimpar 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( r .- q ) =/= .0. )
66 2 1 5 3 deg1nn0cl 
 |-  ( ( R e. Ring /\ ( r .- q ) e. B /\ ( r .- q ) =/= .0. ) -> ( D ` ( r .- q ) ) e. NN0 )
67 56 59 65 66 syl3anc 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` ( r .- q ) ) e. NN0 )
68 nn0addge1 
 |-  ( ( ( D ` G ) e. RR /\ ( D ` ( r .- q ) ) e. NN0 ) -> ( D ` G ) <_ ( ( D ` G ) + ( D ` ( r .- q ) ) ) )
69 55 67 68 syl2anc 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` G ) <_ ( ( D ` G ) + ( D ` ( r .- q ) ) ) )
70 9 ad2antrr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> G e. B )
71 10 ad2antrr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> G =/= .0. )
72 11 ad2antrr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( ( coe1 ` G ) ` ( D ` G ) ) e. E )
73 2 1 12 3 6 5 56 70 71 72 59 65 deg1mul2 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` ( G .xb ( r .- q ) ) ) = ( ( D ` G ) + ( D ` ( r .- q ) ) ) )
74 69 73 breqtrrd 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` G ) <_ ( D ` ( G .xb ( r .- q ) ) ) )
75 ringabl 
 |-  ( P e. Ring -> P e. Abel )
76 15 75 syl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> P e. Abel )
77 3 4 76 18 22 27 ablnnncan1 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) = ( ( G .xb r ) .- ( G .xb q ) ) )
78 3 6 4 15 19 25 20 ringsubdi 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( G .xb ( r .- q ) ) = ( ( G .xb r ) .- ( G .xb q ) ) )
79 77 78 eqtr4d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) = ( G .xb ( r .- q ) ) )
80 79 fveq2d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) = ( D ` ( G .xb ( r .- q ) ) ) )
81 80 adantr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) = ( D ` ( G .xb ( r .- q ) ) ) )
82 74 81 breqtrrd 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( D ` G ) <_ ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) )
83 40 33 xrlenltd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( D ` G ) <_ ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) <-> -. ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) ) )
84 83 adantr 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> ( ( D ` G ) <_ ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) <-> -. ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) ) )
85 82 84 mpbid 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ q =/= r ) -> -. ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) )
86 85 ex 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q =/= r -> -. ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) ) )
87 86 necon4ad 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( D ` ( ( F .- ( G .xb q ) ) .- ( F .- ( G .xb r ) ) ) ) < ( D ` G ) -> q = r ) )
88 51 87 syld 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) -> q = r ) )
89 88 ralrimivva 
 |-  ( ph -> A. q e. B A. r e. B ( ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) -> q = r ) )
90 oveq2 
 |-  ( q = r -> ( G .xb q ) = ( G .xb r ) )
91 90 oveq2d 
 |-  ( q = r -> ( F .- ( G .xb q ) ) = ( F .- ( G .xb r ) ) )
92 91 fveq2d 
 |-  ( q = r -> ( D ` ( F .- ( G .xb q ) ) ) = ( D ` ( F .- ( G .xb r ) ) ) )
93 92 breq1d 
 |-  ( q = r -> ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) <-> ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) )
94 93 rmo4 
 |-  ( E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) <-> A. q e. B A. r e. B ( ( ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ ( D ` ( F .- ( G .xb r ) ) ) < ( D ` G ) ) -> q = r ) )
95 89 94 sylibr 
 |-  ( ph -> E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )