Metamath Proof Explorer

Theorem deg1sublt

Description: Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses deg1sublt.d 
|- D = ( deg1 ` R )
deg1sublt.p 
|- P = ( Poly1 ` R )
deg1sublt.b 
|- B = ( Base ` P )
deg1sublt.m 
|- .- = ( -g ` P )
deg1sublt.l 
|- ( ph -> L e. NN0 )
deg1sublt.r 
|- ( ph -> R e. Ring )
deg1sublt.fb 
|- ( ph -> F e. B )
deg1sublt.fd 
|- ( ph -> ( D ` F ) <_ L )
deg1sublt.gb 
|- ( ph -> G e. B )
deg1sublt.gd 
|- ( ph -> ( D ` G ) <_ L )
deg1sublt.a 
|- A = ( coe1 ` F )
deg1sublt.c 
|- C = ( coe1 ` G )
deg1sublt.eq 
|- ( ph -> ( ( coe1 ` F ) ` L ) = ( ( coe1 ` G ) ` L ) )
Assertion deg1sublt 
|- ( ph -> ( D ` ( F .- G ) ) < L )

Proof

Step Hyp Ref Expression
1 deg1sublt.d 
 |-  D = ( deg1 ` R )
2 deg1sublt.p 
 |-  P = ( Poly1 ` R )
3 deg1sublt.b 
 |-  B = ( Base ` P )
4 deg1sublt.m 
 |-  .- = ( -g ` P )
5 deg1sublt.l 
 |-  ( ph -> L e. NN0 )
6 deg1sublt.r 
 |-  ( ph -> R e. Ring )
7 deg1sublt.fb 
 |-  ( ph -> F e. B )
8 deg1sublt.fd 
 |-  ( ph -> ( D ` F ) <_ L )
9 deg1sublt.gb 
 |-  ( ph -> G e. B )
10 deg1sublt.gd 
 |-  ( ph -> ( D ` G ) <_ L )
11 deg1sublt.a 
 |-  A = ( coe1 ` F )
12 deg1sublt.c 
 |-  C = ( coe1 ` G )
13 deg1sublt.eq 
 |-  ( ph -> ( ( coe1 ` F ) ` L ) = ( ( coe1 ` G ) ` L ) )
14 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 eqid 
 |-  ( coe1 ` ( F .- G ) ) = ( coe1 ` ( F .- G ) )
17 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
18 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
19 6 17 18 3syl 
 |-  ( ph -> P e. Grp )
20 3 4 grpsubcl 
 |-  ( ( P e. Grp /\ F e. B /\ G e. B ) -> ( F .- G ) e. B )
21 19 7 9 20 syl3anc 
 |-  ( ph -> ( F .- G ) e. B )
22 eqid 
 |-  ( -g ` R ) = ( -g ` R )
23 2 3 4 22 coe1subfv 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ L e. NN0 ) -> ( ( coe1 ` ( F .- G ) ) ` L ) = ( ( ( coe1 ` F ) ` L ) ( -g ` R ) ( ( coe1 ` G ) ` L ) ) )
24 6 7 9 5 23 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( F .- G ) ) ` L ) = ( ( ( coe1 ` F ) ` L ) ( -g ` R ) ( ( coe1 ` G ) ` L ) ) )
25 13 oveq1d 
 |-  ( ph -> ( ( ( coe1 ` F ) ` L ) ( -g ` R ) ( ( coe1 ` G ) ` L ) ) = ( ( ( coe1 ` G ) ` L ) ( -g ` R ) ( ( coe1 ` G ) ` L ) ) )
26 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
27 6 26 syl 
 |-  ( ph -> R e. Grp )
28 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
29 eqid 
 |-  ( Base ` R ) = ( Base ` R )
30 28 3 2 29 coe1f 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
31 9 30 syl 
 |-  ( ph -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
32 31 5 ffvelrnd 
 |-  ( ph -> ( ( coe1 ` G ) ` L ) e. ( Base ` R ) )
33 29 15 22 grpsubid 
 |-  ( ( R e. Grp /\ ( ( coe1 ` G ) ` L ) e. ( Base ` R ) ) -> ( ( ( coe1 ` G ) ` L ) ( -g ` R ) ( ( coe1 ` G ) ` L ) ) = ( 0g ` R ) )
34 27 32 33 syl2anc 
 |-  ( ph -> ( ( ( coe1 ` G ) ` L ) ( -g ` R ) ( ( coe1 ` G ) ` L ) ) = ( 0g ` R ) )
35 24 25 34 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( F .- G ) ) ` L ) = ( 0g ` R ) )
36 1 2 14 3 15 16 6 21 5 35 deg1ldgn 
 |-  ( ph -> ( D ` ( F .- G ) ) =/= L )
37 36 neneqd 
 |-  ( ph -> -. ( D ` ( F .- G ) ) = L )
38 1 2 3 deg1xrcl 
 |-  ( ( F .- G ) e. B -> ( D ` ( F .- G ) ) e. RR* )
39 21 38 syl 
 |-  ( ph -> ( D ` ( F .- G ) ) e. RR* )
40 1 2 3 deg1xrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
41 9 40 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
42 1 2 3 deg1xrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
43 7 42 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
44 41 43 ifcld 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* )
45 5 nn0red 
 |-  ( ph -> L e. RR )
46 45 rexrd 
 |-  ( ph -> L e. RR* )
47 2 1 6 3 4 7 9 deg1suble 
 |-  ( ph -> ( D ` ( F .- G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
48 xrmaxle 
 |-  ( ( ( D ` F ) e. RR* /\ ( D ` G ) e. RR* /\ L e. RR* ) -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <_ L <-> ( ( D ` F ) <_ L /\ ( D ` G ) <_ L ) ) )
49 43 41 46 48 syl3anc 
 |-  ( ph -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <_ L <-> ( ( D ` F ) <_ L /\ ( D ` G ) <_ L ) ) )
50 8 10 49 mpbir2and 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <_ L )
51 39 44 46 47 50 xrletrd 
 |-  ( ph -> ( D ` ( F .- G ) ) <_ L )
52 xrleloe 
 |-  ( ( ( D ` ( F .- G ) ) e. RR* /\ L e. RR* ) -> ( ( D ` ( F .- G ) ) <_ L <-> ( ( D ` ( F .- G ) ) < L \/ ( D ` ( F .- G ) ) = L ) ) )
53 39 46 52 syl2anc 
 |-  ( ph -> ( ( D ` ( F .- G ) ) <_ L <-> ( ( D ` ( F .- G ) ) < L \/ ( D ` ( F .- G ) ) = L ) ) )
54 51 53 mpbid 
 |-  ( ph -> ( ( D ` ( F .- G ) ) < L \/ ( D ` ( F .- G ) ) = L ) )
55 orel2 
 |-  ( -. ( D ` ( F .- G ) ) = L -> ( ( ( D ` ( F .- G ) ) < L \/ ( D ` ( F .- G ) ) = L ) -> ( D ` ( F .- G ) ) < L ) )
56 37 54 55 sylc 
 |-  ( ph -> ( D ` ( F .- G ) ) < L )