This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = ( 𝐼 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 )