Metamath Proof Explorer

Theorem dgrsub2

Description: Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Hypothesis dgrsub2.a 
|- N = ( deg ` F )
Assertion dgrsub2 
|- ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( deg ` ( F oF - G ) ) < N )

Proof

Step Hyp Ref Expression
1 dgrsub2.a 
 |-  N = ( deg ` F )
2 simpr2 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> N e. NN )
3 dgr0 
 |-  ( deg ` 0p ) = 0
4 nngt0 
 |-  ( N e. NN -> 0 < N )
5 3 4 eqbrtrid 
 |-  ( N e. NN -> ( deg ` 0p ) < N )
6 fveq2 
 |-  ( ( F oF - G ) = 0p -> ( deg ` ( F oF - G ) ) = ( deg ` 0p ) )
7 6 breq1d 
 |-  ( ( F oF - G ) = 0p -> ( ( deg ` ( F oF - G ) ) < N <-> ( deg ` 0p ) < N ) )
8 5 7 syl5ibrcom 
 |-  ( N e. NN -> ( ( F oF - G ) = 0p -> ( deg ` ( F oF - G ) ) < N ) )
9 2 8 syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( F oF - G ) = 0p -> ( deg ` ( F oF - G ) ) < N ) )
10 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
11 10 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
12 plyssc 
 |-  ( Poly ` T ) C_ ( Poly ` CC )
13 12 sseli 
 |-  ( G e. ( Poly ` T ) -> G e. ( Poly ` CC ) )
14 eqid 
 |-  ( deg ` F ) = ( deg ` F )
15 eqid 
 |-  ( deg ` G ) = ( deg ` G )
16 14 15 dgrsub 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) ) -> ( deg ` ( F oF - G ) ) <_ if ( ( deg ` F ) <_ ( deg ` G ) , ( deg ` G ) , ( deg ` F ) ) )
17 11 13 16 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) -> ( deg ` ( F oF - G ) ) <_ if ( ( deg ` F ) <_ ( deg ` G ) , ( deg ` G ) , ( deg ` F ) ) )
18 17 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( deg ` ( F oF - G ) ) <_ if ( ( deg ` F ) <_ ( deg ` G ) , ( deg ` G ) , ( deg ` F ) ) )
19 simpr1 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( deg ` G ) = N )
20 1 eqcomi 
 |-  ( deg ` F ) = N
21 20 a1i 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( deg ` F ) = N )
22 19 21 ifeq12d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> if ( ( deg ` F ) <_ ( deg ` G ) , ( deg ` G ) , ( deg ` F ) ) = if ( ( deg ` F ) <_ ( deg ` G ) , N , N ) )
23 ifid 
 |-  if ( ( deg ` F ) <_ ( deg ` G ) , N , N ) = N
24 22 23 eqtrdi 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> if ( ( deg ` F ) <_ ( deg ` G ) , ( deg ` G ) , ( deg ` F ) ) = N )
25 18 24 breqtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( deg ` ( F oF - G ) ) <_ N )
26 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
27 eqid 
 |-  ( coeff ` G ) = ( coeff ` G )
28 26 27 coesub 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) ) -> ( coeff ` ( F oF - G ) ) = ( ( coeff ` F ) oF - ( coeff ` G ) ) )
29 11 13 28 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) -> ( coeff ` ( F oF - G ) ) = ( ( coeff ` F ) oF - ( coeff ` G ) ) )
30 29 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( coeff ` ( F oF - G ) ) = ( ( coeff ` F ) oF - ( coeff ` G ) ) )
31 30 fveq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( coeff ` ( F oF - G ) ) ` N ) = ( ( ( coeff ` F ) oF - ( coeff ` G ) ) ` N ) )
32 2 nnnn0d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> N e. NN0 )
33 26 coef3 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
34 33 ad2antrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( coeff ` F ) : NN0 --> CC )
35 34 ffnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( coeff ` F ) Fn NN0 )
36 27 coef3 
 |-  ( G e. ( Poly ` T ) -> ( coeff ` G ) : NN0 --> CC )
37 36 ad2antlr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( coeff ` G ) : NN0 --> CC )
38 37 ffnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( coeff ` G ) Fn NN0 )
39 nn0ex 
 |-  NN0 e. _V
40 39 a1i 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> NN0 e. _V )
41 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
42 simplr3 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) /\ N e. NN0 ) -> ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) )
43 eqidd 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) /\ N e. NN0 ) -> ( ( coeff ` G ) ` N ) = ( ( coeff ` G ) ` N ) )
44 35 38 40 40 41 42 43 ofval 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) /\ N e. NN0 ) -> ( ( ( coeff ` F ) oF - ( coeff ` G ) ) ` N ) = ( ( ( coeff ` G ) ` N ) - ( ( coeff ` G ) ` N ) ) )
45 32 44 mpdan 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( ( coeff ` F ) oF - ( coeff ` G ) ) ` N ) = ( ( ( coeff ` G ) ` N ) - ( ( coeff ` G ) ` N ) ) )
46 37 32 ffvelrnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( coeff ` G ) ` N ) e. CC )
47 46 subidd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( ( coeff ` G ) ` N ) - ( ( coeff ` G ) ` N ) ) = 0 )
48 31 45 47 3eqtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( coeff ` ( F oF - G ) ) ` N ) = 0 )
49 plysubcl 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) ) -> ( F oF - G ) e. ( Poly ` CC ) )
50 11 13 49 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) -> ( F oF - G ) e. ( Poly ` CC ) )
51 50 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( F oF - G ) e. ( Poly ` CC ) )
52 eqid 
 |-  ( deg ` ( F oF - G ) ) = ( deg ` ( F oF - G ) )
53 eqid 
 |-  ( coeff ` ( F oF - G ) ) = ( coeff ` ( F oF - G ) )
54 52 53 dgrlt 
 |-  ( ( ( F oF - G ) e. ( Poly ` CC ) /\ N e. NN0 ) -> ( ( ( F oF - G ) = 0p \/ ( deg ` ( F oF - G ) ) < N ) <-> ( ( deg ` ( F oF - G ) ) <_ N /\ ( ( coeff ` ( F oF - G ) ) ` N ) = 0 ) ) )
55 51 32 54 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( ( F oF - G ) = 0p \/ ( deg ` ( F oF - G ) ) < N ) <-> ( ( deg ` ( F oF - G ) ) <_ N /\ ( ( coeff ` ( F oF - G ) ) ` N ) = 0 ) ) )
56 25 48 55 mpbir2and 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( ( F oF - G ) = 0p \/ ( deg ` ( F oF - G ) ) < N ) )
57 56 ord 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( -. ( F oF - G ) = 0p -> ( deg ` ( F oF - G ) ) < N ) )
58 9 57 pm2.61d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` T ) ) /\ ( ( deg ` G ) = N /\ N e. NN /\ ( ( coeff ` F ) ` N ) = ( ( coeff ` G ) ` N ) ) ) -> ( deg ` ( F oF - G ) ) < N )