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. )