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 ˙ = 0 R
mdegval.a A = m 0 I | m -1 Fin
mdegval.h H = h A fld h
mdeglt.f φ F B
medglt.x φ X A
mdeglt.lt φ D F < H X
Assertion mdeglt φ 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 ˙ = 0 R
5 mdegval.a A = m 0 I | m -1 Fin
6 mdegval.h H = h A fld h
7 mdeglt.f φ F B
8 medglt.x φ X A
9 mdeglt.lt φ 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 B D F = sup H F supp 0 ˙ * <
15 7 14 syl φ D F = sup H F supp 0 ˙ * <
16 imassrn H F supp 0 ˙ ran H
17 5 6 tdeglem1 H : A 0
18 frn H : A 0 ran H 0
19 17 18 mp1i φ ran H 0
20 nn0ssre 0
21 ressxr *
22 20 21 sstri 0 *
23 19 22 sstrdi φ ran H *
24 16 23 sstrid φ H F supp 0 ˙ *
25 supxrcl H F supp 0 ˙ * sup H F supp 0 ˙ * < *
26 24 25 syl φ sup H F supp 0 ˙ * < *
27 15 26 eqeltrd φ D F *
28 27 xrleidd φ D F D F
29 1 2 3 4 5 6 mdegleb F B D F * D F D F x A D F < H x F x = 0 ˙
30 7 27 29 syl2anc φ D F D F x A D F < H x F x = 0 ˙
31 28 30 mpbid φ x A D F < H x F x = 0 ˙
32 13 31 8 rspcdva φ D F < H X F X = 0 ˙
33 9 32 mpd φ F X = 0 ˙