Metamath Proof Explorer

Theorem deg1add

Description: Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses deg1addle.y 
|- Y = ( Poly1 ` R )
deg1addle.d 
|- D = ( deg1 ` R )
deg1addle.r 
|- ( ph -> R e. Ring )
deg1addle.b 
|- B = ( Base ` Y )
deg1addle.p 
|- .+ = ( +g ` Y )
deg1addle.f 
|- ( ph -> F e. B )
deg1addle.g 
|- ( ph -> G e. B )
deg1add.l 
|- ( ph -> ( D ` G ) < ( D ` F ) )
Assertion deg1add 
|- ( ph -> ( D ` ( F .+ G ) ) = ( D ` F ) )

Proof

Step Hyp Ref Expression
1 deg1addle.y 
 |-  Y = ( Poly1 ` R )
2 deg1addle.d 
 |-  D = ( deg1 ` R )
3 deg1addle.r 
 |-  ( ph -> R e. Ring )
4 deg1addle.b 
 |-  B = ( Base ` Y )
5 deg1addle.p 
 |-  .+ = ( +g ` Y )
6 deg1addle.f 
 |-  ( ph -> F e. B )
7 deg1addle.g 
 |-  ( ph -> G e. B )
8 deg1add.l 
 |-  ( ph -> ( D ` G ) < ( D ` F ) )
9 1 ply1ring 
 |-  ( R e. Ring -> Y e. Ring )
10 3 9 syl 
 |-  ( ph -> Y e. Ring )
11 4 5 ringacl 
 |-  ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .+ G ) e. B )
12 10 6 7 11 syl3anc 
 |-  ( ph -> ( F .+ G ) e. B )
13 2 1 4 deg1xrcl 
 |-  ( ( F .+ G ) e. B -> ( D ` ( F .+ G ) ) e. RR* )
14 12 13 syl 
 |-  ( ph -> ( D ` ( F .+ G ) ) e. RR* )
15 2 1 4 deg1xrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
16 6 15 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
17 1 2 3 4 5 6 7 deg1addle 
 |-  ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
18 2 1 4 deg1xrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
19 7 18 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
20 xrltnle 
 |-  ( ( ( D ` G ) e. RR* /\ ( D ` F ) e. RR* ) -> ( ( D ` G ) < ( D ` F ) <-> -. ( D ` F ) <_ ( D ` G ) ) )
21 19 16 20 syl2anc 
 |-  ( ph -> ( ( D ` G ) < ( D ` F ) <-> -. ( D ` F ) <_ ( D ` G ) ) )
22 8 21 mpbid 
 |-  ( ph -> -. ( D ` F ) <_ ( D ` G ) )
23 22 iffalsed 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) = ( D ` F ) )
24 17 23 breqtrd 
 |-  ( ph -> ( D ` ( F .+ G ) ) <_ ( D ` F ) )
25 nltmnf 
 |-  ( ( D ` G ) e. RR* -> -. ( D ` G ) < -oo )
26 19 25 syl 
 |-  ( ph -> -. ( D ` G ) < -oo )
27 8 adantr 
 |-  ( ( ph /\ F = ( 0g ` Y ) ) -> ( D ` G ) < ( D ` F ) )
28 fveq2 
 |-  ( F = ( 0g ` Y ) -> ( D ` F ) = ( D ` ( 0g ` Y ) ) )
29 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
30 2 1 29 deg1z 
 |-  ( R e. Ring -> ( D ` ( 0g ` Y ) ) = -oo )
31 3 30 syl 
 |-  ( ph -> ( D ` ( 0g ` Y ) ) = -oo )
32 28 31 sylan9eqr 
 |-  ( ( ph /\ F = ( 0g ` Y ) ) -> ( D ` F ) = -oo )
33 27 32 breqtrd 
 |-  ( ( ph /\ F = ( 0g ` Y ) ) -> ( D ` G ) < -oo )
34 33 ex 
 |-  ( ph -> ( F = ( 0g ` Y ) -> ( D ` G ) < -oo ) )
35 34 necon3bd 
 |-  ( ph -> ( -. ( D ` G ) < -oo -> F =/= ( 0g ` Y ) ) )
36 26 35 mpd 
 |-  ( ph -> F =/= ( 0g ` Y ) )
37 2 1 29 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= ( 0g ` Y ) ) -> ( D ` F ) e. NN0 )
38 3 6 36 37 syl3anc 
 |-  ( ph -> ( D ` F ) e. NN0 )
39 eqid 
 |-  ( +g ` R ) = ( +g ` R )
40 1 4 5 39 coe1addfv 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ ( D ` F ) e. NN0 ) -> ( ( coe1 ` ( F .+ G ) ) ` ( D ` F ) ) = ( ( ( coe1 ` F ) ` ( D ` F ) ) ( +g ` R ) ( ( coe1 ` G ) ` ( D ` F ) ) ) )
41 3 6 7 38 40 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( F .+ G ) ) ` ( D ` F ) ) = ( ( ( coe1 ` F ) ` ( D ` F ) ) ( +g ` R ) ( ( coe1 ` G ) ` ( D ` F ) ) ) )
42 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
43 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
44 2 1 4 42 43 deg1lt 
 |-  ( ( G e. B /\ ( D ` F ) e. NN0 /\ ( D ` G ) < ( D ` F ) ) -> ( ( coe1 ` G ) ` ( D ` F ) ) = ( 0g ` R ) )
45 7 38 8 44 syl3anc 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` F ) ) = ( 0g ` R ) )
46 45 oveq2d 
 |-  ( ph -> ( ( ( coe1 ` F ) ` ( D ` F ) ) ( +g ` R ) ( ( coe1 ` G ) ` ( D ` F ) ) ) = ( ( ( coe1 ` F ) ` ( D ` F ) ) ( +g ` R ) ( 0g ` R ) ) )
47 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
48 3 47 syl 
 |-  ( ph -> R e. Grp )
49 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
50 eqid 
 |-  ( Base ` R ) = ( Base ` R )
51 49 4 1 50 coe1f 
 |-  ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
52 6 51 syl 
 |-  ( ph -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
53 52 38 ffvelrnd 
 |-  ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) e. ( Base ` R ) )
54 50 39 42 grprid 
 |-  ( ( R e. Grp /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. ( Base ` R ) ) -> ( ( ( coe1 ` F ) ` ( D ` F ) ) ( +g ` R ) ( 0g ` R ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) )
55 48 53 54 syl2anc 
 |-  ( ph -> ( ( ( coe1 ` F ) ` ( D ` F ) ) ( +g ` R ) ( 0g ` R ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) )
56 41 46 55 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( F .+ G ) ) ` ( D ` F ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) )
57 2 1 29 4 42 49 deg1ldg 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= ( 0g ` Y ) ) -> ( ( coe1 ` F ) ` ( D ` F ) ) =/= ( 0g ` R ) )
58 3 6 36 57 syl3anc 
 |-  ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) =/= ( 0g ` R ) )
59 56 58 eqnetrd 
 |-  ( ph -> ( ( coe1 ` ( F .+ G ) ) ` ( D ` F ) ) =/= ( 0g ` R ) )
60 eqid 
 |-  ( coe1 ` ( F .+ G ) ) = ( coe1 ` ( F .+ G ) )
61 2 1 4 42 60 deg1ge 
 |-  ( ( ( F .+ G ) e. B /\ ( D ` F ) e. NN0 /\ ( ( coe1 ` ( F .+ G ) ) ` ( D ` F ) ) =/= ( 0g ` R ) ) -> ( D ` F ) <_ ( D ` ( F .+ G ) ) )
62 12 38 59 61 syl3anc 
 |-  ( ph -> ( D ` F ) <_ ( D ` ( F .+ G ) ) )
63 14 16 24 62 xrletrid 
 |-  ( ph -> ( D ` ( F .+ G ) ) = ( D ` F ) )