| Step | Hyp | Ref
| Expression |
| 1 | | mdegval.d |
. . . . 5
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
| 2 | | mdegval.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
| 3 | | mdegval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
| 4 | | mdegval.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
| 5 | | mdegval.a |
. . . . 5
⊢ 𝐴 = {𝑚 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑚 “ ℕ) ∈
Fin} |
| 6 | | mdegval.h |
. . . . 5
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) |
| 7 | 1, 2, 3, 4, 5, 6 | mdegval 26102 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
| 9 | 8 | breq1d 5153 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺)) |
| 10 | | imassrn 6089 |
. . . 4
⊢ (𝐻 “ (𝐹 supp 0 )) ⊆ ran 𝐻 |
| 11 | 5, 6 | tdeglem1 26097 |
. . . . . . 7
⊢ 𝐻:𝐴⟶ℕ0 |
| 12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐻:𝐴⟶ℕ0) |
| 13 | 12 | frnd 6744 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ran
𝐻 ⊆
ℕ0) |
| 14 | | nn0ssre 12530 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
| 15 | | ressxr 11305 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
| 16 | 14, 15 | sstri 3993 |
. . . . 5
⊢
ℕ0 ⊆ ℝ* |
| 17 | 13, 16 | sstrdi 3996 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ran
𝐻 ⊆
ℝ*) |
| 18 | 10, 17 | sstrid 3995 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) |
| 19 | | supxrleub 13368 |
. . 3
⊢ (((𝐻 “ (𝐹 supp 0 )) ⊆
ℝ* ∧ 𝐺
∈ ℝ*) → (sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺 ↔
∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺)) |
| 20 | 18, 19 | sylancom 588 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺 ↔
∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺)) |
| 21 | 12 | ffnd 6737 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐻 Fn 𝐴) |
| 22 | | suppssdm 8202 |
. . . . 5
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
| 23 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 24 | | simpl 482 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹 ∈ 𝐵) |
| 25 | 2, 23, 3, 5, 24 | mplelf 22018 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹:𝐴⟶(Base‘𝑅)) |
| 26 | 22, 25 | fssdm 6755 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐹 supp 0 ) ⊆ 𝐴) |
| 27 | | breq1 5146 |
. . . . 5
⊢ (𝑦 = (𝐻‘𝑥) → (𝑦 ≤ 𝐺 ↔ (𝐻‘𝑥) ≤ 𝐺)) |
| 28 | 27 | ralima 7257 |
. . . 4
⊢ ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) ⊆ 𝐴) → (∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺)) |
| 29 | 21, 26, 28 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺)) |
| 30 | 25 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹 Fn 𝐴) |
| 31 | 4 | fvexi 6920 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 0 ∈
V) |
| 33 | | elsuppfng 8194 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 ∈ 𝐵 ∧ 0 ∈ V) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ))) |
| 34 | 30, 24, 32, 33 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ))) |
| 35 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ V |
| 36 | 35 | biantrur 530 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ≠ 0 ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 )) |
| 37 | | eldifsn 4786 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 )) |
| 38 | 36, 37 | bitr4i 278 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) ∈ (V ∖ { 0 })) |
| 39 | 38 | anbi2i 623 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 }))) |
| 40 | 34, 39 | bitrdi 287 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
| 41 | 40 | imbi1d 341 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ (𝐹 supp 0 ) → (𝐻‘𝑥) ≤ 𝐺) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺))) |
| 42 | | impexp 450 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺))) |
| 43 | | con34b 316 |
. . . . . . . 8
⊢ (((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺) ↔ (¬ (𝐻‘𝑥) ≤ 𝐺 → ¬ (𝐹‘𝑥) ∈ (V ∖ { 0 }))) |
| 44 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈
ℝ*) |
| 45 | 12 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℕ0) |
| 46 | 16, 45 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
| 47 | | xrltnle 11328 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ*
∧ (𝐻‘𝑥) ∈ ℝ*)
→ (𝐺 < (𝐻‘𝑥) ↔ ¬ (𝐻‘𝑥) ≤ 𝐺)) |
| 48 | 44, 46, 47 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐺 < (𝐻‘𝑥) ↔ ¬ (𝐻‘𝑥) ≤ 𝐺)) |
| 49 | 48 | bicomd 223 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐻‘𝑥) ≤ 𝐺 ↔ 𝐺 < (𝐻‘𝑥))) |
| 50 | | ianor 984 |
. . . . . . . . . . 11
⊢ (¬
((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 ) ↔ (¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 )) |
| 51 | 50, 37 | xchnxbir 333 |
. . . . . . . . . 10
⊢ (¬
(𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ (¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 )) |
| 52 | | orcom 871 |
. . . . . . . . . . . 12
⊢ ((¬
(𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (¬ (𝐹‘𝑥) ≠ 0 ∨ ¬ (𝐹‘𝑥) ∈ V)) |
| 53 | 35 | notnoti 143 |
. . . . . . . . . . . . 13
⊢ ¬
¬ (𝐹‘𝑥) ∈ V |
| 54 | 53 | biorfri 940 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹‘𝑥) ≠ 0 ↔ (¬ (𝐹‘𝑥) ≠ 0 ∨ ¬ (𝐹‘𝑥) ∈ V)) |
| 55 | | nne 2944 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) = 0 ) |
| 56 | 52, 54, 55 | 3bitr2i 299 |
. . . . . . . . . . 11
⊢ ((¬
(𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (𝐹‘𝑥) = 0 ) |
| 57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → ((¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (𝐹‘𝑥) = 0 )) |
| 58 | 51, 57 | bitrid 283 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ (𝐹‘𝑥) = 0 )) |
| 59 | 49, 58 | imbi12d 344 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → ((¬ (𝐻‘𝑥) ≤ 𝐺 → ¬ (𝐹‘𝑥) ∈ (V ∖ { 0 })) ↔ (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
| 60 | 43, 59 | bitrid 283 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
| 61 | 60 | pm5.74da 804 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺)) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
| 62 | 42, 61 | bitrid 283 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
| 63 | 41, 62 | bitrd 279 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ (𝐹 supp 0 ) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
| 64 | 63 | ralbidv2 3174 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
| 65 | 29, 64 | bitrd 279 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
| 66 | 9, 20, 65 | 3bitrd 305 |
1
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |