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	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
	mdegval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mdegval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mdegval.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mdegval.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
	mdegval.h	⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
	mdeglt.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	medglt.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	mdeglt.lt	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑋 ) )
Assertion	mdeglt	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		mdegval.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
2		mdegval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mdegval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mdegval.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		mdegval.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
6		mdegval.h	⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
7		mdeglt.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		medglt.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
9		mdeglt.lt	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑋 ) )
10		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑋 ) )
11	10	breq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑥 ) ↔ ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑋 ) ) )
12		fveqeq2	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑋 ) = 0 ) )
13	11 12	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑋 ) = 0 ) ) )
14	1 2 3 4 5 6	mdegval	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
15	7 14	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
16		imassrn	⊢ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ran 𝐻
17	5 6	tdeglem1	⊢ 𝐻 : 𝐴 ⟶ ℕ0
18		frn	⊢ ( 𝐻 : 𝐴 ⟶ ℕ0 → ran 𝐻 ⊆ ℕ0 )
19	17 18	mp1i	⊢ ( 𝜑 → ran 𝐻 ⊆ ℕ0 )
20		nn0ssre	⊢ ℕ0 ⊆ ℝ
21		ressxr	⊢ ℝ ⊆ ℝ*
22	20 21	sstri	⊢ ℕ0 ⊆ ℝ*
23	19 22	sstrdi	⊢ ( 𝜑 → ran 𝐻 ⊆ ℝ* )
24	16 23	sstrid	⊢ ( 𝜑 → ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* )
25		supxrcl	⊢ ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ℝ* )
26	24 25	syl	⊢ ( 𝜑 → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ℝ* )
27	15 26	eqeltrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
28	27	xrleidd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) )
29	1 2 3 4 5 6	mdegleb	⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
30	7 27 29	syl2anc	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
31	28 30	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) )
32	13 31 8	rspcdva	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) < ( 𝐻 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑋 ) = 0 ) )
33	9 32	mpd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 0 )