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

Metamath Proof Explorer

Theorem mdegnn0cl

Description: Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdeg0.d 
|- D = ( I mDeg R )
mdeg0.p 
|- P = ( I mPoly R )
mdeg0.z 
|- .0. = ( 0g ` P )
mdegnn0cl.b 
|- B = ( Base ` P )
Assertion mdegnn0cl 
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )

Proof

Step Hyp Ref Expression
1 mdeg0.d 
 |-  D = ( I mDeg R )
2 mdeg0.p 
 |-  P = ( I mPoly R )
3 mdeg0.z 
 |-  .0. = ( 0g ` P )
4 mdegnn0cl.b 
 |-  B = ( Base ` P )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 eqid 
 |-  { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
7 eqid 
 |-  ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) = ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) )
8 1 2 4 5 6 7 3 mdegldg 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> E. x e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } ( ( F ` x ) =/= ( 0g ` R ) /\ ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) = ( D ` F ) ) )
9 6 7 tdeglem1 
 |-  ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) : { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } --> NN0
10 9 a1i 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) : { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } --> NN0 )
11 10 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ x e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } ) -> ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) e. NN0 )
12 eleq1 
 |-  ( ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) = ( D ` F ) -> ( ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) e. NN0 <-> ( D ` F ) e. NN0 ) )
13 11 12 syl5ibcom 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ x e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } ) -> ( ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) = ( D ` F ) -> ( D ` F ) e. NN0 ) )
14 13 adantld 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ x e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } ) -> ( ( ( F ` x ) =/= ( 0g ` R ) /\ ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) = ( D ` F ) ) -> ( D ` F ) e. NN0 ) )
15 14 rexlimdva 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. x e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } ( ( F ` x ) =/= ( 0g ` R ) /\ ( ( h e. { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } |-> ( CCfld gsum h ) ) ` x ) = ( D ` F ) ) -> ( D ` F ) e. NN0 ) )
16 8 15 mpd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )