Metamath Proof Explorer


Theorem mdegle0

Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y
|- Y = ( I mPoly R )
mdegaddle.d
|- D = ( I mDeg R )
mdegaddle.i
|- ( ph -> I e. V )
mdegaddle.r
|- ( ph -> R e. Ring )
mdegle0.b
|- B = ( Base ` Y )
mdegle0.a
|- A = ( algSc ` Y )
mdegle0.f
|- ( ph -> F e. B )
Assertion mdegle0
|- ( ph -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( F ` ( I X. { 0 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y
 |-  Y = ( I mPoly R )
2 mdegaddle.d
 |-  D = ( I mDeg R )
3 mdegaddle.i
 |-  ( ph -> I e. V )
4 mdegaddle.r
 |-  ( ph -> R e. Ring )
5 mdegle0.b
 |-  B = ( Base ` Y )
6 mdegle0.a
 |-  A = ( algSc ` Y )
7 mdegle0.f
 |-  ( ph -> F e. B )
8 0xr
 |-  0 e. RR*
9 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
10 eqid
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
11 eqid
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) )
12 2 1 5 9 10 11 mdegleb
 |-  ( ( F e. B /\ 0 e. RR* ) -> ( ( D ` F ) <_ 0 <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( F ` x ) = ( 0g ` R ) ) ) )
13 7 8 12 sylancl
 |-  ( ph -> ( ( D ` F ) <_ 0 <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( F ` x ) = ( 0g ` R ) ) ) )
14 10 11 tdeglem1
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0
15 14 a1i
 |-  ( ph -> ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0 )
16 15 ffvelrnda
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. NN0 )
17 nn0re
 |-  ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. NN0 -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. RR )
18 nn0ge0
 |-  ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. NN0 -> 0 <_ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) )
19 17 18 jca
 |-  ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. NN0 -> ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. RR /\ 0 <_ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) )
20 ne0gt0
 |-  ( ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) e. RR /\ 0 <_ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) -> ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) =/= 0 <-> 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) )
21 16 19 20 3syl
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) =/= 0 <-> 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) )
22 10 11 tdeglem4
 |-  ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } -> ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) = 0 <-> x = ( I X. { 0 } ) ) )
23 22 adantl
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) = 0 <-> x = ( I X. { 0 } ) ) )
24 23 necon3abid
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) =/= 0 <-> -. x = ( I X. { 0 } ) ) )
25 21 24 bitr3d
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) <-> -. x = ( I X. { 0 } ) ) )
26 25 imbi1d
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( F ` x ) = ( 0g ` R ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
27 eqeq2
 |-  ( ( F ` ( I X. { 0 } ) ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) -> ( ( F ` x ) = ( F ` ( I X. { 0 } ) ) <-> ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
28 27 bibi1d
 |-  ( ( F ` ( I X. { 0 } ) ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) -> ( ( ( F ` x ) = ( F ` ( I X. { 0 } ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) <-> ( ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) ) )
29 eqeq2
 |-  ( ( 0g ` R ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) -> ( ( F ` x ) = ( 0g ` R ) <-> ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
30 29 bibi1d
 |-  ( ( 0g ` R ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) -> ( ( ( F ` x ) = ( 0g ` R ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) <-> ( ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) ) )
31 fveq2
 |-  ( x = ( I X. { 0 } ) -> ( F ` x ) = ( F ` ( I X. { 0 } ) ) )
32 pm2.24
 |-  ( x = ( I X. { 0 } ) -> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) )
33 31 32 2thd
 |-  ( x = ( I X. { 0 } ) -> ( ( F ` x ) = ( F ` ( I X. { 0 } ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
34 33 adantl
 |-  ( ( ph /\ x = ( I X. { 0 } ) ) -> ( ( F ` x ) = ( F ` ( I X. { 0 } ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
35 biimt
 |-  ( -. x = ( I X. { 0 } ) -> ( ( F ` x ) = ( 0g ` R ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
36 35 adantl
 |-  ( ( ph /\ -. x = ( I X. { 0 } ) ) -> ( ( F ` x ) = ( 0g ` R ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
37 28 30 34 36 ifbothda
 |-  ( ph -> ( ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
38 37 adantr
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) <-> ( -. x = ( I X. { 0 } ) -> ( F ` x ) = ( 0g ` R ) ) ) )
39 26 38 bitr4d
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( F ` x ) = ( 0g ` R ) ) <-> ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
40 39 ralbidva
 |-  ( ph -> ( A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( F ` x ) = ( 0g ` R ) ) <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
41 eqid
 |-  ( Base ` R ) = ( Base ` R )
42 1 41 5 10 7 mplelf
 |-  ( ph -> F : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
43 42 feqmptd
 |-  ( ph -> F = ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( F ` x ) ) )
44 10 psrbag0
 |-  ( I e. V -> ( I X. { 0 } ) e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
45 3 44 syl
 |-  ( ph -> ( I X. { 0 } ) e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
46 42 45 ffvelrnd
 |-  ( ph -> ( F ` ( I X. { 0 } ) ) e. ( Base ` R ) )
47 1 10 9 41 6 3 4 46 mplascl
 |-  ( ph -> ( A ` ( F ` ( I X. { 0 } ) ) ) = ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
48 43 47 eqeq12d
 |-  ( ph -> ( F = ( A ` ( F ` ( I X. { 0 } ) ) ) <-> ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( F ` x ) ) = ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) ) )
49 fvex
 |-  ( F ` x ) e. _V
50 49 rgenw
 |-  A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( F ` x ) e. _V
51 mpteqb
 |-  ( A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( F ` x ) e. _V -> ( ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( F ` x ) ) = ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
52 50 51 mp1i
 |-  ( ph -> ( ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( F ` x ) ) = ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
53 48 52 bitrd
 |-  ( ph -> ( F = ( A ` ( F ` ( I X. { 0 } ) ) ) <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( F ` x ) = if ( x = ( I X. { 0 } ) , ( F ` ( I X. { 0 } ) ) , ( 0g ` R ) ) ) )
54 40 53 bitr4d
 |-  ( ph -> ( A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( 0 < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( F ` x ) = ( 0g ` R ) ) <-> F = ( A ` ( F ` ( I X. { 0 } ) ) ) ) )
55 13 54 bitrd
 |-  ( ph -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( F ` ( I X. { 0 } ) ) ) ) )