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 
 |-  ( I e. V -> ( 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 3 14 syl 
 |-  ( 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 
 |-  ( ( I e. V /\ 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 3 22 sylan 
 |-  ( ( 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 } ) ) ) ) )