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 24584 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
8 | 7 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
9 | 8 | breq1d 5067 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺)) |
10 | | imassrn 5933 |
. . . 4
⊢ (𝐻 “ (𝐹 supp 0 )) ⊆ ran 𝐻 |
11 | 2, 3 | mplrcl 20198 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐼 ∈ V) |
13 | 5, 6 | tdeglem1 24579 |
. . . . . . 7
⊢ (𝐼 ∈ V → 𝐻:𝐴⟶ℕ0) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐻:𝐴⟶ℕ0) |
15 | 14 | frnd 6514 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ran
𝐻 ⊆
ℕ0) |
16 | | nn0ssre 11889 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
17 | | ressxr 10673 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
18 | 16, 17 | sstri 3973 |
. . . . 5
⊢
ℕ0 ⊆ ℝ* |
19 | 15, 18 | sstrdi 3976 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ran
𝐻 ⊆
ℝ*) |
20 | 10, 19 | sstrid 3975 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) |
21 | | supxrleub 12707 |
. . 3
⊢ (((𝐻 “ (𝐹 supp 0 )) ⊆
ℝ* ∧ 𝐺
∈ ℝ*) → (sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺 ↔
∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺)) |
22 | 20, 21 | sylancom 588 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺 ↔
∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺)) |
23 | 14 | ffnd 6508 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐻 Fn 𝐴) |
24 | | suppssdm 7832 |
. . . . 5
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
25 | | eqid 2818 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
26 | | simpl 483 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹 ∈ 𝐵) |
27 | 2, 25, 3, 5, 26 | mplelf 20141 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹:𝐴⟶(Base‘𝑅)) |
28 | 24, 27 | fssdm 6523 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐹 supp 0 ) ⊆ 𝐴) |
29 | | breq1 5060 |
. . . . 5
⊢ (𝑦 = (𝐻‘𝑥) → (𝑦 ≤ 𝐺 ↔ (𝐻‘𝑥) ≤ 𝐺)) |
30 | 29 | ralima 6991 |
. . . 4
⊢ ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) ⊆ 𝐴) → (∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺)) |
31 | 23, 28, 30 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺)) |
32 | 27 | ffnd 6508 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹 Fn 𝐴) |
33 | | ovex 7178 |
. . . . . . . . . 10
⊢
(ℕ0 ↑m 𝐼) ∈ V |
34 | 33 | rabex 5226 |
. . . . . . . . 9
⊢ {𝑚 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑚 “ ℕ) ∈ Fin} ∈
V |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → {𝑚 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑚 “ ℕ) ∈ Fin} ∈
V) |
36 | 5, 35 | eqeltrid 2914 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐴 ∈ V) |
37 | 4 | fvexi 6677 |
. . . . . . . 8
⊢ 0 ∈
V |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 0 ∈
V) |
39 | | elsuppfn 7827 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ))) |
40 | | fvex 6676 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
41 | 40 | biantrur 531 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ≠ 0 ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 )) |
42 | | eldifsn 4711 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 )) |
43 | 41, 42 | bitr4i 279 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) ∈ (V ∖ { 0 })) |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → ((𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) ∈ (V ∖ { 0 }))) |
45 | 44 | anbi2d 628 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
46 | 39, 45 | bitrd 280 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
47 | 32, 36, 38, 46 | syl3anc 1363 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
48 | 47 | imbi1d 343 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ (𝐹 supp 0 ) → (𝐻‘𝑥) ≤ 𝐺) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺))) |
49 | | impexp 451 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺))) |
50 | | con34b 317 |
. . . . . . . 8
⊢ (((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺) ↔ (¬ (𝐻‘𝑥) ≤ 𝐺 → ¬ (𝐹‘𝑥) ∈ (V ∖ { 0 }))) |
51 | | simplr 765 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈
ℝ*) |
52 | 14 | ffvelrnda 6843 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℕ0) |
53 | 18, 52 | sseldi 3962 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
54 | | xrltnle 10696 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ*
∧ (𝐻‘𝑥) ∈ ℝ*)
→ (𝐺 < (𝐻‘𝑥) ↔ ¬ (𝐻‘𝑥) ≤ 𝐺)) |
55 | 51, 53, 54 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐺 < (𝐻‘𝑥) ↔ ¬ (𝐻‘𝑥) ≤ 𝐺)) |
56 | 55 | bicomd 224 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐻‘𝑥) ≤ 𝐺 ↔ 𝐺 < (𝐻‘𝑥))) |
57 | | ianor 975 |
. . . . . . . . . . 11
⊢ (¬
((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 ) ↔ (¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 )) |
58 | 57, 42 | xchnxbir 334 |
. . . . . . . . . 10
⊢ (¬
(𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ (¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 )) |
59 | | orcom 864 |
. . . . . . . . . . . 12
⊢ ((¬
(𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (¬ (𝐹‘𝑥) ≠ 0 ∨ ¬ (𝐹‘𝑥) ∈ V)) |
60 | 40 | notnoti 145 |
. . . . . . . . . . . . 13
⊢ ¬
¬ (𝐹‘𝑥) ∈ V |
61 | 60 | biorfi 932 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹‘𝑥) ≠ 0 ↔ (¬ (𝐹‘𝑥) ≠ 0 ∨ ¬ (𝐹‘𝑥) ∈ V)) |
62 | | nne 3017 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) = 0 ) |
63 | 59, 61, 62 | 3bitr2i 300 |
. . . . . . . . . . 11
⊢ ((¬
(𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (𝐹‘𝑥) = 0 ) |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → ((¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (𝐹‘𝑥) = 0 )) |
65 | 58, 64 | syl5bb 284 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ (𝐹‘𝑥) = 0 )) |
66 | 56, 65 | imbi12d 346 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → ((¬ (𝐻‘𝑥) ≤ 𝐺 → ¬ (𝐹‘𝑥) ∈ (V ∖ { 0 })) ↔ (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
67 | 50, 66 | syl5bb 284 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
68 | 67 | pm5.74da 800 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺)) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
69 | 49, 68 | syl5bb 284 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
70 | 48, 69 | bitrd 280 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ (𝐹 supp 0 ) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
71 | 70 | ralbidv2 3192 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
72 | 31, 71 | bitrd 280 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
73 | 9, 22, 72 | 3bitrd 306 |
1
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |