Metamath Proof Explorer

Theorem dgrsub

Description: The degree of a difference of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses dgrsub.1 
|- M = ( deg ` F )
dgrsub.2 
|- N = ( deg ` G )
Assertion dgrsub 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF - G ) ) <_ if ( M <_ N , N , M ) )

Proof

Step Hyp Ref Expression
1 dgrsub.1 
 |-  M = ( deg ` F )
2 dgrsub.2 
 |-  N = ( deg ` G )
3 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
4 3 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
5 ssid 
 |-  CC C_ CC
6 neg1cn 
 |-  -u 1 e. CC
7 plyconst 
 |-  ( ( CC C_ CC /\ -u 1 e. CC ) -> ( CC X. { -u 1 } ) e. ( Poly ` CC ) )
8 5 6 7 mp2an 
 |-  ( CC X. { -u 1 } ) e. ( Poly ` CC )
9 3 sseli 
 |-  ( G e. ( Poly ` S ) -> G e. ( Poly ` CC ) )
10 plymulcl 
 |-  ( ( ( CC X. { -u 1 } ) e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) ) -> ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` CC ) )
11 8 9 10 sylancr 
 |-  ( G e. ( Poly ` S ) -> ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` CC ) )
12 eqid 
 |-  ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) )
13 1 12 dgradd 
 |-  ( ( F e. ( Poly ` CC ) /\ ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` CC ) ) -> ( deg ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) <_ if ( M <_ ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) , ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) , M ) )
14 4 11 13 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) <_ if ( M <_ ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) , ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) , M ) )
15 cnex 
 |-  CC e. _V
16 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
17 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
18 ofnegsub 
 |-  ( ( CC e. _V /\ F : CC --> CC /\ G : CC --> CC ) -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
19 15 16 17 18 mp3an3an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
20 19 fveq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) = ( deg ` ( F oF - G ) ) )
21 neg1ne0 
 |-  -u 1 =/= 0
22 dgrmulc 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ G e. ( Poly ` S ) ) -> ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( deg ` G ) )
23 6 21 22 mp3an12 
 |-  ( G e. ( Poly ` S ) -> ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( deg ` G ) )
24 23 2 eqtr4di 
 |-  ( G e. ( Poly ` S ) -> ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) = N )
25 24 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) = N )
26 25 breq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( M <_ ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) <-> M <_ N ) )
27 26 25 ifbieq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> if ( M <_ ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) , ( deg ` ( ( CC X. { -u 1 } ) oF x. G ) ) , M ) = if ( M <_ N , N , M ) )
28 14 20 27 3brtr3d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF - G ) ) <_ if ( M <_ N , N , M ) )