Metamath Proof Explorer

Theorem deg1tm

Description: Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses deg1tm.d 
|- D = ( deg1 ` R )
deg1tm.k 
|- K = ( Base ` R )
deg1tm.p 
|- P = ( Poly1 ` R )
deg1tm.x 
|- X = ( var1 ` R )
deg1tm.m 
|- .x. = ( .s ` P )
deg1tm.n 
|- N = ( mulGrp ` P )
deg1tm.e 
|- .^ = ( .g ` N )
deg1tm.z 
|- .0. = ( 0g ` R )
Assertion deg1tm 
|- ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) = F )

Proof

Step Hyp Ref Expression
1 deg1tm.d 
 |-  D = ( deg1 ` R )
2 deg1tm.k 
 |-  K = ( Base ` R )
3 deg1tm.p 
 |-  P = ( Poly1 ` R )
4 deg1tm.x 
 |-  X = ( var1 ` R )
5 deg1tm.m 
 |-  .x. = ( .s ` P )
6 deg1tm.n 
 |-  N = ( mulGrp ` P )
7 deg1tm.e 
 |-  .^ = ( .g ` N )
8 deg1tm.z 
 |-  .0. = ( 0g ` R )
9 eqid 
 |-  ( Base ` P ) = ( Base ` P )
10 2 3 4 5 6 7 9 ply1tmcl 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( C .x. ( F .^ X ) ) e. ( Base ` P ) )
11 10 3adant2r 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( C .x. ( F .^ X ) ) e. ( Base ` P ) )
12 1 3 9 deg1xrcl 
 |-  ( ( C .x. ( F .^ X ) ) e. ( Base ` P ) -> ( D ` ( C .x. ( F .^ X ) ) ) e. RR* )
13 11 12 syl 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) e. RR* )
14 simp3 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> F e. NN0 )
15 14 nn0red 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> F e. RR )
16 15 rexrd 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> F e. RR* )
17 1 2 3 4 5 6 7 deg1tmle 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) <_ F )
18 17 3adant2r 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) <_ F )
19 8 2 3 4 5 6 7 coe1tmfv1 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` F ) = C )
20 19 3adant2r 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` F ) = C )
21 simp2r 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> C =/= .0. )
22 20 21 eqnetrd 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` F ) =/= .0. )
23 eqid 
 |-  ( coe1 ` ( C .x. ( F .^ X ) ) ) = ( coe1 ` ( C .x. ( F .^ X ) ) )
24 1 3 9 8 23 deg1ge 
 |-  ( ( ( C .x. ( F .^ X ) ) e. ( Base ` P ) /\ F e. NN0 /\ ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` F ) =/= .0. ) -> F <_ ( D ` ( C .x. ( F .^ X ) ) ) )
25 11 14 22 24 syl3anc 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> F <_ ( D ` ( C .x. ( F .^ X ) ) ) )
26 13 16 18 25 xrletrid 
 |-  ( ( R e. Ring /\ ( C e. K /\ C =/= .0. ) /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) = F )