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\mathrm{mDeg}R$$
	mdegval.p	$$⊢P=I\mathrm{mPoly}R$$
	mdegval.b	$$⊢B={\mathrm{Base}}_P$$
	mdegval.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mdegval.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mdegval.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
	mdeglt.f	$$⊢\phi \to F\in B$$
	medglt.x	$$⊢\phi \to X\in A$$
	mdeglt.lt	$$⊢\phi \to D\left(F\right)<H\left(X\right)$$
Assertion	mdeglt	$$⊢\phi \to F\left(X\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		mdegval.d	$$⊢D=I\mathrm{mDeg}R$$
2		mdegval.p	$$⊢P=I\mathrm{mPoly}R$$
3		mdegval.b	$$⊢B={\mathrm{Base}}_P$$
4		mdegval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		mdegval.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mdegval.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
7		mdeglt.f	$$⊢\phi \to F\in B$$
8		medglt.x	$$⊢\phi \to X\in A$$
9		mdeglt.lt	$$⊢\phi \to D\left(F\right)<H\left(X\right)$$
10		fveq2	$$⊢x=X\to H\left(x\right)=H\left(X\right)$$
11	10	breq2d	$$⊢x=X\to \left(D\left(F\right)<H\left(x\right)\leftrightarrow D\left(F\right)<H\left(X\right)\right)$$
12		fveqeq2	$$⊢x=X\to \left(F\left(x\right)=\underset{\dot{}}{0}\leftrightarrow F\left(X\right)=\underset{\dot{}}{0}\right)$$
13	11 12	imbi12d	$$⊢x=X\to \left(\left(D\left(F\right)<H\left(x\right)\to F\left(x\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(D\left(F\right)<H\left(X\right)\to F\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
14	1 2 3 4 5 6	mdegval	$$⊢F\in B\to D\left(F\right)=sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)$$
15	7 14	syl	$$⊢\phi \to D\left(F\right)=sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)$$
16		imassrn	$$⊢H\left[F\mathrm{supp}\underset{\dot{}}{0}\right]\subseteq \mathrm{ran}H$$
17	5 6	tdeglem1	$$⊢H:A⟶{\mathbb{N}}_0$$
18		frn	$$⊢H:A⟶{\mathbb{N}}_0\to \mathrm{ran}H\subseteq {\mathbb{N}}_0$$
19	17 18	mp1i	$$⊢\phi \to \mathrm{ran}H\subseteq {\mathbb{N}}_0$$
20		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
21		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
22	20 21	sstri	$$⊢{\mathbb{N}}_0\subseteq {ℝ}^{*}$$
23	19 22	sstrdi	$$⊢\phi \to \mathrm{ran}H\subseteq {ℝ}^{*}$$
24	16 23	sstrid	$$⊢\phi \to H\left[F\mathrm{supp}\underset{\dot{}}{0}\right]\subseteq {ℝ}^{*}$$
25		supxrcl	$$⊢H\left[F\mathrm{supp}\underset{\dot{}}{0}\right]\subseteq {ℝ}^{*}\to sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)\in {ℝ}^{*}$$
26	24 25	syl	$$⊢\phi \to sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)\in {ℝ}^{*}$$
27	15 26	eqeltrd	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
28	27	xrleidd	$$⊢\phi \to D\left(F\right)\le D\left(F\right)$$
29	1 2 3 4 5 6	mdegleb	$$⊢\left(F\in B\wedge D\left(F\right)\in {ℝ}^{*}\right)\to \left(D\left(F\right)\le D\left(F\right)\leftrightarrow \forall x\in A\left(D\left(F\right)<H\left(x\right)\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
30	7 27 29	syl2anc	$$⊢\phi \to \left(D\left(F\right)\le D\left(F\right)\leftrightarrow \forall x\in A\left(D\left(F\right)<H\left(x\right)\to F\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
31	28 30	mpbid	$$⊢\phi \to \forall x\in A\left(D\left(F\right)<H\left(x\right)\to F\left(x\right)=\underset{\dot{}}{0}\right)$$
32	13 31 8	rspcdva	$$⊢\phi \to \left(D\left(F\right)<H\left(X\right)\to F\left(X\right)=\underset{\dot{}}{0}\right)$$
33	9 32	mpd	$$⊢\phi \to F\left(X\right)=\underset{\dot{}}{0}$$