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 simp1 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> R e. Ring )
15 2 3 4 13 14 mplelsfi 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F finSupp .0. )
16 15 fsuppimpd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( F supp .0. ) e. Fin )
17 imafi 
 |-  ( ( Fun H /\ ( F supp .0. ) e. Fin ) -> ( H " ( F supp .0. ) ) e. Fin )
18 12 16 17 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) e. Fin )
19 simp3 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F =/= Y )
20 2 3 mplrcl 
 |-  ( F e. B -> I e. _V )
21 20 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> I e. _V )
22 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
23 22 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> R e. Grp )
24 2 5 4 7 21 23 mpl0 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> Y = ( A X. { .0. } ) )
25 19 24 neeqtrd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F =/= ( A X. { .0. } ) )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 2 26 3 5 13 mplelf 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F : A --> ( Base ` R ) )
28 27 ffnd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> F Fn A )
29 4 fvexi 
 |-  .0. e. _V
30 ovex 
 |-  ( NN0 ^m I ) e. _V
31 5 30 rabex2 
 |-  A e. _V
32 fnsuppeq0 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( ( F supp .0. ) = (/) <-> F = ( A X. { .0. } ) ) )
33 31 32 mp3an2 
 |-  ( ( F Fn A /\ .0. e. _V ) -> ( ( F supp .0. ) = (/) <-> F = ( A X. { .0. } ) ) )
34 28 29 33 sylancl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( F supp .0. ) = (/) <-> F = ( A X. { .0. } ) ) )
35 34 necon3bid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( F supp .0. ) =/= (/) <-> F =/= ( A X. { .0. } ) ) )
36 25 35 mpbird 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( F supp .0. ) =/= (/) )
37 11 ffnd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> H Fn A )
38 suppssdm 
 |-  ( F supp .0. ) C_ dom F
39 38 27 fssdm 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( F supp .0. ) C_ A )
40 fnimaeq0 
 |-  ( ( H Fn A /\ ( F supp .0. ) C_ A ) -> ( ( H " ( F supp .0. ) ) = (/) <-> ( F supp .0. ) = (/) ) )
41 37 39 40 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( H " ( F supp .0. ) ) = (/) <-> ( F supp .0. ) = (/) ) )
42 41 necon3bid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( ( H " ( F supp .0. ) ) =/= (/) <-> ( F supp .0. ) =/= (/) ) )
43 36 42 mpbird 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) =/= (/) )
44 imassrn 
 |-  ( H " ( F supp .0. ) ) C_ ran H
45 11 frnd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ran H C_ NN0 )
46 44 45 sstrid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) C_ NN0 )
47 nn0ssre 
 |-  NN0 C_ RR
48 ressxr 
 |-  RR C_ RR*
49 47 48 sstri 
 |-  NN0 C_ RR*
50 46 49 sstrdi 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( H " ( F supp .0. ) ) C_ RR* )
51 xrltso 
 |-  < Or RR*
52 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. ) ) )
53 51 52 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. ) ) )
54 18 43 50 53 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. ( H " ( F supp .0. ) ) )
55 9 54 eqeltrd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> ( D ` F ) e. ( H " ( F supp .0. ) ) )
56 37 39 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 ) ) )
57 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 ) ) ) )
58 31 29 57 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 ) ) ) )
59 28 58 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 ) ) ) )
60 56 59 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 ) ) ) )
61 55 60 mpbid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) )