Metamath Proof Explorer

Theorem mdegldg

Description: A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdegval.d 
|- D = ( I mDeg R )
mdegval.p 
|- P = ( I mPoly R )
mdegval.b 
|- B = ( Base ` P )
mdegval.z 
|- .0. = ( 0g ` R )
mdegval.a 
|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
mdegval.h 
|- H = ( h e. A |-> ( CCfld gsum h ) )
mdegldg.y 
|- Y = ( 0g ` P )
Assertion mdegldg 
|- ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) )

Proof

Step Hyp Ref Expression
1 mdegval.d 
 |-  D = ( I mDeg R )
2 mdegval.p 
 |-  P = ( I mPoly R )
3 mdegval.b 
 |-  B = ( Base ` P )
4 mdegval.z 
 |-  .0. = ( 0g ` R )
5 mdegval.a 
 |-  A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
6 mdegval.h 
 |-  H = ( h e. A |-> ( CCfld gsum h ) )
7 mdegldg.y 
 |-  Y = ( 0g ` P )
8 1 2 3 4 5 6 mdegval 
 |-  ( F e. B -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
9 8 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
10 5 6 tdeglem1 
 |-  H : A --> NN0
11 10 a1i 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> H : A --> NN0 )
12 11 ffund 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> Fun H )
13 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F e. B )
14 2 3 4 13 mplelsfi 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F finSupp .0. )
15 14 fsuppimpd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( F supp .0. ) e. Fin )
16 imafi 
 |-  ( ( Fun H /\ ( F supp .0. ) e. Fin ) -> ( H " ( F supp .0. ) ) e. Fin )
17 12 15 16 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) e. Fin )
18 simp3 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F =/= Y )
19 2 3 mplrcl 
 |-  ( F e. B -> I e. _V )
20 19 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> I e. _V )
21 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
22 21 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> R e. Grp )
23 2 5 4 7 20 22 mpl0 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> Y = ( A X. { .0. } ) )
24 18 23 neeqtrd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F =/= ( A X. { .0. } ) )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 2 25 3 5 13 mplelf 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F : A --> ( Base ` R ) )
27 26 ffnd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F Fn A )
28 4 fvexi 
 |-  .0. e. _V
29 ovex 
 |-  ( NN0 ^m I ) e. _V
30 5 29 rabex2 
 |-  A e. _V
31 fnsuppeq0 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( ( F supp .0. ) = (/) <-> F = ( A X. { .0. } ) ) )
32 30 31 mp3an2 
 |-  ( ( F Fn A /\ .0. e. _V ) -> ( ( F supp .0. ) = (/) <-> F = ( A X. { .0. } ) ) )
33 27 28 32 sylancl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( F supp .0. ) = (/) <-> F = ( A X. { .0. } ) ) )
34 33 necon3bid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( F supp .0. ) =/= (/) <-> F =/= ( A X. { .0. } ) ) )
35 24 34 mpbird 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( F supp .0. ) =/= (/) )
36 11 ffnd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> H Fn A )
37 suppssdm 
 |-  ( F supp .0. ) C_ dom F
38 37 26 fssdm 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( F supp .0. ) C_ A )
39 fnimaeq0 
 |-  ( ( H Fn A /\ ( F supp .0. ) C_ A ) -> ( ( H " ( F supp .0. ) ) = (/) <-> ( F supp .0. ) = (/) ) )
40 36 38 39 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( H " ( F supp .0. ) ) = (/) <-> ( F supp .0. ) = (/) ) )
41 40 necon3bid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( H " ( F supp .0. ) ) =/= (/) <-> ( F supp .0. ) =/= (/) ) )
42 35 41 mpbird 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) =/= (/) )
43 imassrn 
 |-  ( H " ( F supp .0. ) ) C_ ran H
44 11 frnd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ran H C_ NN0 )
45 43 44 sstrid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) C_ NN0 )
46 nn0ssre 
 |-  NN0 C_ RR
47 ressxr 
 |-  RR C_ RR*
48 46 47 sstri 
 |-  NN0 C_ RR*
49 45 48 sstrdi 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) C_ RR* )
50 xrltso 
 |-  < Or RR*
51 fisupcl 
 |-  ( ( < Or RR* /\ ( ( H " ( F supp .0. ) ) e. Fin /\ ( H " ( F supp .0. ) ) =/= (/) /\ ( H " ( F supp .0. ) ) C_ RR* ) ) -> sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. ( H " ( F supp .0. ) ) )
52 50 51 mpan 
 |-  ( ( ( H " ( F supp .0. ) ) e. Fin /\ ( H " ( F supp .0. ) ) =/= (/) /\ ( H " ( F supp .0. ) ) C_ RR* ) -> sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. ( H " ( F supp .0. ) ) )
53 17 42 49 52 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. ( H " ( F supp .0. ) ) )
54 9 53 eqeltrd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( D ` F ) e. ( H " ( F supp .0. ) ) )
55 36 38 fvelimabd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( D ` F ) e. ( H " ( F supp .0. ) ) <-> E. x e. ( F supp .0. ) ( H ` x ) = ( D ` F ) ) )
56 rexsupp 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( E. x e. ( F supp .0. ) ( H ` x ) = ( D ` F ) <-> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) ) )
57 30 28 56 mp3an23 
 |-  ( F Fn A -> ( E. x e. ( F supp .0. ) ( H ` x ) = ( D ` F ) <-> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) ) )
58 27 57 syl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( E. x e. ( F supp .0. ) ( H ` x ) = ( D ` F ) <-> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) ) )
59 55 58 bitrd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( D ` F ) e. ( H " ( F supp .0. ) ) <-> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) ) )
60 54 59 mpbid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) )