Metamath Proof Explorer

Theorem mdeglt

Description: If there is an upper limit on the degree of a polynomial that is lower than the degree of some exponent bag, then that exponent bag is unrepresented in the polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

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 ) )
mdeglt.f 
|- ( ph -> F e. B )
medglt.x 
|- ( ph -> X e. A )
mdeglt.lt 
|- ( ph -> ( D ` F ) < ( H ` X ) )
Assertion mdeglt 
|- ( ph -> ( F ` X ) = .0. )

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 mdeglt.f 
 |-  ( ph -> F e. B )
8 medglt.x 
 |-  ( ph -> X e. A )
9 mdeglt.lt 
 |-  ( ph -> ( D ` F ) < ( H ` X ) )
10 fveq2 
 |-  ( x = X -> ( H ` x ) = ( H ` X ) )
11 10 breq2d 
 |-  ( x = X -> ( ( D ` F ) < ( H ` x ) <-> ( D ` F ) < ( H ` X ) ) )
12 fveqeq2 
 |-  ( x = X -> ( ( F ` x ) = .0. <-> ( F ` X ) = .0. ) )
13 11 12 imbi12d 
 |-  ( x = X -> ( ( ( D ` F ) < ( H ` x ) -> ( F ` x ) = .0. ) <-> ( ( D ` F ) < ( H ` X ) -> ( F ` X ) = .0. ) ) )
14 1 2 3 4 5 6 mdegval 
 |-  ( F e. B -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
15 7 14 syl 
 |-  ( ph -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
16 imassrn 
 |-  ( H " ( F supp .0. ) ) C_ ran H
17 5 6 tdeglem1 
 |-  H : A --> NN0
18 frn 
 |-  ( H : A --> NN0 -> ran H C_ NN0 )
19 17 18 mp1i 
 |-  ( ph -> ran H C_ NN0 )
20 nn0ssre 
 |-  NN0 C_ RR
21 ressxr 
 |-  RR C_ RR*
22 20 21 sstri 
 |-  NN0 C_ RR*
23 19 22 sstrdi 
 |-  ( ph -> ran H C_ RR* )
24 16 23 sstrid 
 |-  ( ph -> ( H " ( F supp .0. ) ) C_ RR* )
25 supxrcl 
 |-  ( ( H " ( F supp .0. ) ) C_ RR* -> sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. RR* )
26 24 25 syl 
 |-  ( ph -> sup ( ( H " ( F supp .0. ) ) , RR* , < ) e. RR* )
27 15 26 eqeltrd 
 |-  ( ph -> ( D ` F ) e. RR* )
28 27 xrleidd 
 |-  ( ph -> ( D ` F ) <_ ( D ` F ) )
29 1 2 3 4 5 6 mdegleb 
 |-  ( ( F e. B /\ ( D ` F ) e. RR* ) -> ( ( D ` F ) <_ ( D ` F ) <-> A. x e. A ( ( D ` F ) < ( H ` x ) -> ( F ` x ) = .0. ) ) )
30 7 27 29 syl2anc 
 |-  ( ph -> ( ( D ` F ) <_ ( D ` F ) <-> A. x e. A ( ( D ` F ) < ( H ` x ) -> ( F ` x ) = .0. ) ) )
31 28 30 mpbid 
 |-  ( ph -> A. x e. A ( ( D ` F ) < ( H ` x ) -> ( F ` x ) = .0. ) )
32 13 31 8 rspcdva 
 |-  ( ph -> ( ( D ` F ) < ( H ` X ) -> ( F ` X ) = .0. ) )
33 9 32 mpd 
 |-  ( ph -> ( F ` X ) = .0. )