Metamath Proof Explorer

Theorem deg1tmle

Description: Limiting 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 )
Assertion deg1tmle 
|- ( ( R e. Ring /\ C e. K /\ 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 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 simpl1 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> R e. Ring )
10 simpl2 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> C e. K )
11 simpl3 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> F e. NN0 )
12 simprl 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> x e. NN0 )
13 11 nn0red 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> F e. RR )
14 simprr 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> F < x )
15 13 14 ltned 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> F =/= x )
16 8 2 3 4 5 6 7 9 10 11 12 15 coe1tmfv2 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ ( x e. NN0 /\ F < x ) ) -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` x ) = ( 0g ` R ) )
17 16 expr 
 |-  ( ( ( R e. Ring /\ C e. K /\ F e. NN0 ) /\ x e. NN0 ) -> ( F < x -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` x ) = ( 0g ` R ) ) )
18 17 ralrimiva 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> A. x e. NN0 ( F < x -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` x ) = ( 0g ` R ) ) )
19 eqid 
 |-  ( Base ` P ) = ( Base ` P )
20 2 3 4 5 6 7 19 ply1tmcl 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( C .x. ( F .^ X ) ) e. ( Base ` P ) )
21 nn0re 
 |-  ( F e. NN0 -> F e. RR )
22 21 rexrd 
 |-  ( F e. NN0 -> F e. RR* )
23 22 3ad2ant3 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> F e. RR* )
24 eqid 
 |-  ( coe1 ` ( C .x. ( F .^ X ) ) ) = ( coe1 ` ( C .x. ( F .^ X ) ) )
25 1 3 19 8 24 deg1leb 
 |-  ( ( ( C .x. ( F .^ X ) ) e. ( Base ` P ) /\ F e. RR* ) -> ( ( D ` ( C .x. ( F .^ X ) ) ) <_ F <-> A. x e. NN0 ( F < x -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` x ) = ( 0g ` R ) ) ) )
26 20 23 25 syl2anc 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( ( D ` ( C .x. ( F .^ X ) ) ) <_ F <-> A. x e. NN0 ( F < x -> ( ( coe1 ` ( C .x. ( F .^ X ) ) ) ` x ) = ( 0g ` R ) ) ) )
27 18 26 mpbird 
 |-  ( ( R e. Ring /\ C e. K /\ F e. NN0 ) -> ( D ` ( C .x. ( F .^ X ) ) ) <_ F )