This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem deg1pwle

Description: Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses deg1pw.d 
|- D = ( deg1 ` R )
deg1pw.p 
|- P = ( Poly1 ` R )
deg1pw.x 
|- X = ( var1 ` R )
deg1pw.n 
|- N = ( mulGrp ` P )
deg1pw.e 
|- .^ = ( .g ` N )
Assertion deg1pwle 
|- ( ( R e. Ring /\ F e. NN0 ) -> ( D ` ( F .^ X ) ) <_ F )

Proof

Step Hyp Ref Expression
1 deg1pw.d 
 |-  D = ( deg1 ` R )
2 deg1pw.p 
 |-  P = ( Poly1 ` R )
3 deg1pw.x 
 |-  X = ( var1 ` R )
4 deg1pw.n 
 |-  N = ( mulGrp ` P )
5 deg1pw.e 
 |-  .^ = ( .g ` N )
6 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
8 2 3 4 5 7 ply1moncl 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> ( F .^ X ) e. ( Base ` P ) )
9 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
10 eqid 
 |-  ( .s ` P ) = ( .s ` P )
11 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
12 7 9 10 11 lmodvs1 
 |-  ( ( P e. LMod /\ ( F .^ X ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( F .^ X ) ) = ( F .^ X ) )
13 6 8 12 syl2an2r 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( F .^ X ) ) = ( F .^ X ) )
14 13 fveq2d 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> ( D ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( F .^ X ) ) ) = ( D ` ( F .^ X ) ) )
15 simpl 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> R e. Ring )
16 2 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
17 16 fveq2d 
 |-  ( R e. Ring -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 18 19 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
21 17 20 eqeltrrd 
 |-  ( R e. Ring -> ( 1r ` ( Scalar ` P ) ) e. ( Base ` R ) )
22 21 adantr 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> ( 1r ` ( Scalar ` P ) ) e. ( Base ` R ) )
23 simpr 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> F e. NN0 )
24 1 18 2 3 10 4 5 deg1tmle 
 |-  ( ( R e. Ring /\ ( 1r ` ( Scalar ` P ) ) e. ( Base ` R ) /\ F e. NN0 ) -> ( D ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( F .^ X ) ) ) <_ F )
25 15 22 23 24 syl3anc 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> ( D ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( F .^ X ) ) ) <_ F )
26 14 25 eqbrtrrd 
 |-  ( ( R e. Ring /\ F e. NN0 ) -> ( D ` ( F .^ X ) ) <_ F )