Metamath Proof Explorer

Theorem mdegleb

Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015)

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 ℎ ) )
Assertion mdegleb ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 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 1 2 3 4 5 6 mdegval ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
8 7 adantr ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
9 8 breq1d ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐺 ↔ sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ≤ 𝐺 ) )
10 imassrn ⊢ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ran 𝐻
11 2 3 mplrcl ⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
12 11 adantr ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐼 ∈ V )
13 5 6 tdeglem1 ⊢ ( 𝐼 ∈ V → 𝐻 : 𝐴 ⟶ ℕ0 )
14 12 13 syl ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐻 : 𝐴 ⟶ ℕ0 )
15 14 frnd ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ran 𝐻 ⊆ ℕ0 )
16 nn0ssre ⊢ ℕ0 ⊆ ℝ
17 ressxr ⊢ ℝ ⊆ ℝ*
18 16 17 sstri ⊢ ℕ0 ⊆ ℝ*
19 15 18 sstrdi ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ran 𝐻 ⊆ ℝ* )
20 10 19 sstrid ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* )
21 supxrleub ⊢ ( ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* ∧ 𝐺 ∈ ℝ* ) → ( sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ≤ 𝐺 ↔ ∀ 𝑦 ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) 𝑦 ≤ 𝐺 ) )
22 20 21 sylancom ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ≤ 𝐺 ↔ ∀ 𝑦 ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) 𝑦 ≤ 𝐺 ) )
23 14 ffnd ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐻 Fn 𝐴 )
24 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 simpl ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐹 ∈ 𝐵 )
27 2 25 3 5 26 mplelf ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
28 24 27 fssdm ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
29 breq1 ⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( 𝑦 ≤ 𝐺 ↔ ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) )
30 29 ralima ⊢ ( ( 𝐻 Fn 𝐴 ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → ( ∀ 𝑦 ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) 𝑦 ≤ 𝐺 ↔ ∀ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) )
31 23 28 30 syl2anc ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ∀ 𝑦 ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) 𝑦 ≤ 𝐺 ↔ ∀ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) )
32 27 ffnd ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐹 Fn 𝐴 )
33 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
34 33 rabex ⊢ { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin } ∈ V
35 34 a1i ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin } ∈ V )
36 5 35 eqeltrid ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 𝐴 ∈ V )
37 4 fvexi ⊢ 0 ∈ V
38 37 a1i ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → 0 ∈ V )
39 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V ) → ( 𝑥 ∈ ( 𝐹 supp 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) )
40 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
41 40 biantrur ⊢ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) )
42 eldifsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) )
43 41 42 bitr4i ⊢ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) )
44 43 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) )
45 44 anbi2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V ) → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) ) )
46 39 45 bitrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V ) → ( 𝑥 ∈ ( 𝐹 supp 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) ) )
47 32 36 38 46 syl3anc ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐹 supp 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) ) )
48 47 imbi1d ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝐹 supp 0 ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ) )
49 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ↔ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ) )
50 con34b ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ↔ ( ¬ ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 → ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) )
51 simplr ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → 𝐺 ∈ ℝ* )
52 14 ffvelrnda ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ℕ0 )
53 18 52 sseldi ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ* )
54 xrltnle ⊢ ( ( 𝐺 ∈ ℝ* ∧ ( 𝐻 ‘ 𝑥 ) ∈ ℝ* ) → ( 𝐺 < ( 𝐻 ‘ 𝑥 ) ↔ ¬ ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) )
55 51 53 54 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 < ( 𝐻 ‘ 𝑥 ) ↔ ¬ ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) )
56 55 bicomd ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ↔ 𝐺 < ( 𝐻 ‘ 𝑥 ) ) )
57 ianor ⊢ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ↔ ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ∨ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) )
58 57 42 xchnxbir ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ↔ ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ∨ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) )
59 orcom ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ∨ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ↔ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ) )
60 40 notnoti ⊢ ¬ ¬ ( 𝐹 ‘ 𝑥 ) ∈ V
61 60 biorfi ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ) )
62 nne ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 )
63 59 61 62 3bitr2i ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ∨ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ↔ ( 𝐹 ‘ 𝑥 ) = 0 )
64 63 a1i ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ V ∨ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
65 58 64 syl5bb ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
66 56 65 imbi12d ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ¬ ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 → ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) ↔ ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
67 50 66 syl5bb ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ↔ ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
68 67 pm5.74da ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) ) )
69 49 68 syl5bb ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 0 } ) ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) ) )
70 48 69 bitrd ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝐹 supp 0 ) → ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) ) )
71 70 ralbidv2 ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
72 31 71 bitrd ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ∀ 𝑦 ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) 𝑦 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
73 9 22 72 3bitrd ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 < ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )