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