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
↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈
Fin} |
6 | | mdegval.h |
. . . . 5
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) |
7 | 1, 2, 3, 4, 5, 6 | mdegval 23627 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
8 | 7 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
9 | 8 | breq1d 4593 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺)) |
10 | | imassrn 5396 |
. . . 4
⊢ (𝐻 “ (𝐹 supp 0 )) ⊆ ran 𝐻 |
11 | 2, 3 | mplrcl 19311 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐼 ∈ V) |
13 | 5, 6 | tdeglem1 23622 |
. . . . . . 7
⊢ (𝐼 ∈ V → 𝐻:𝐴⟶ℕ0) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐻:𝐴⟶ℕ0) |
15 | | frn 5966 |
. . . . . 6
⊢ (𝐻:𝐴⟶ℕ0 → ran 𝐻 ⊆
ℕ0) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ran
𝐻 ⊆
ℕ0) |
17 | | nn0ssre 11173 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
18 | | ressxr 9962 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
19 | 17, 18 | sstri 3577 |
. . . . 5
⊢
ℕ0 ⊆ ℝ* |
20 | 16, 19 | syl6ss 3580 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ran
𝐻 ⊆
ℝ*) |
21 | 10, 20 | syl5ss 3579 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) |
22 | | supxrleub 12028 |
. . 3
⊢ (((𝐻 “ (𝐹 supp 0 )) ⊆
ℝ* ∧ 𝐺
∈ ℝ*) → (sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺 ↔
∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺)) |
23 | 21, 22 | sylancom 698 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ≤ 𝐺 ↔
∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺)) |
24 | | ffn 5958 |
. . . . 5
⊢ (𝐻:𝐴⟶ℕ0 → 𝐻 Fn 𝐴) |
25 | 14, 24 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐻 Fn 𝐴) |
26 | | suppssdm 7195 |
. . . . 5
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
27 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
28 | | simpl 472 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹 ∈ 𝐵) |
29 | 2, 27, 3, 5, 28 | mplelf 19254 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹:𝐴⟶(Base‘𝑅)) |
30 | | fdm 5964 |
. . . . . 6
⊢ (𝐹:𝐴⟶(Base‘𝑅) → dom 𝐹 = 𝐴) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → dom
𝐹 = 𝐴) |
32 | 26, 31 | syl5sseq 3616 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝐹 supp 0 ) ⊆ 𝐴) |
33 | | breq1 4586 |
. . . . 5
⊢ (𝑦 = (𝐻‘𝑥) → (𝑦 ≤ 𝐺 ↔ (𝐻‘𝑥) ≤ 𝐺)) |
34 | 33 | ralima 6402 |
. . . 4
⊢ ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) ⊆ 𝐴) → (∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺)) |
35 | 25, 32, 34 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺)) |
36 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶(Base‘𝑅) → 𝐹 Fn 𝐴) |
37 | 29, 36 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐹 Fn 𝐴) |
38 | | ovex 6577 |
. . . . . . . . . 10
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
39 | 38 | rabex 4740 |
. . . . . . . . 9
⊢ {𝑚 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} ∈
V |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → {𝑚 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} ∈
V) |
41 | 5, 40 | syl5eqel 2692 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 𝐴 ∈ V) |
42 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝑅) ∈ V |
43 | 4, 42 | eqeltri 2684 |
. . . . . . . 8
⊢ 0 ∈
V |
44 | 43 | a1i 11 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → 0 ∈
V) |
45 | | elsuppfn 7190 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ))) |
46 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
47 | 46 | biantrur 526 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ≠ 0 ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 )) |
48 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 )) |
49 | 47, 48 | bitr4i 266 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) ∈ (V ∖ { 0 })) |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → ((𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) ∈ (V ∖ { 0 }))) |
51 | 50 | anbi2d 736 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
52 | 45, 51 | bitrd 267 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
53 | 37, 41, 44, 52 | syl3anc 1318 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })))) |
54 | 53 | imbi1d 330 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ (𝐹 supp 0 ) → (𝐻‘𝑥) ≤ 𝐺) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺))) |
55 | | impexp 461 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺))) |
56 | | con34b 305 |
. . . . . . . 8
⊢ (((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺) ↔ (¬ (𝐻‘𝑥) ≤ 𝐺 → ¬ (𝐹‘𝑥) ∈ (V ∖ { 0 }))) |
57 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈
ℝ*) |
58 | 14 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℕ0) |
59 | 19, 58 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
60 | | xrltnle 9984 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ*
∧ (𝐻‘𝑥) ∈ ℝ*)
→ (𝐺 < (𝐻‘𝑥) ↔ ¬ (𝐻‘𝑥) ≤ 𝐺)) |
61 | 57, 59, 60 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (𝐺 < (𝐻‘𝑥) ↔ ¬ (𝐻‘𝑥) ≤ 𝐺)) |
62 | 61 | bicomd 212 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐻‘𝑥) ≤ 𝐺 ↔ 𝐺 < (𝐻‘𝑥))) |
63 | | ianor 508 |
. . . . . . . . . . 11
⊢ (¬
((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 0 ) ↔ (¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 )) |
64 | 63, 48 | xchnxbir 322 |
. . . . . . . . . 10
⊢ (¬
(𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ (¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 )) |
65 | | orcom 401 |
. . . . . . . . . . . 12
⊢ ((¬
(𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (¬ (𝐹‘𝑥) ≠ 0 ∨ ¬ (𝐹‘𝑥) ∈ V)) |
66 | 46 | notnoti 136 |
. . . . . . . . . . . . 13
⊢ ¬
¬ (𝐹‘𝑥) ∈ V |
67 | 66 | biorfi 421 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹‘𝑥) ≠ 0 ↔ (¬ (𝐹‘𝑥) ≠ 0 ∨ ¬ (𝐹‘𝑥) ∈ V)) |
68 | | nne 2786 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹‘𝑥) ≠ 0 ↔ (𝐹‘𝑥) = 0 ) |
69 | 65, 67, 68 | 3bitr2i 287 |
. . . . . . . . . . 11
⊢ ((¬
(𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (𝐹‘𝑥) = 0 ) |
70 | 69 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → ((¬ (𝐹‘𝑥) ∈ V ∨ ¬ (𝐹‘𝑥) ≠ 0 ) ↔ (𝐹‘𝑥) = 0 )) |
71 | 64, 70 | syl5bb 271 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) ∈ (V ∖ { 0 }) ↔ (𝐹‘𝑥) = 0 )) |
72 | 62, 71 | imbi12d 333 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → ((¬ (𝐻‘𝑥) ≤ 𝐺 → ¬ (𝐹‘𝑥) ∈ (V ∖ { 0 })) ↔ (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
73 | 56, 72 | syl5bb 271 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) ∧ 𝑥 ∈ 𝐴) → (((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
74 | 73 | pm5.74da 719 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ∈ (V ∖ { 0 }) → (𝐻‘𝑥) ≤ 𝐺)) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
75 | 55, 74 | syl5bb 271 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ { 0 })) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
76 | 54, 75 | bitrd 267 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝑥 ∈ (𝐹 supp 0 ) → (𝐻‘𝑥) ≤ 𝐺) ↔ (𝑥 ∈ 𝐴 → (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))) |
77 | 76 | ralbidv2 2967 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
78 | 35, 77 | bitrd 267 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) →
(∀𝑦 ∈ (𝐻 “ (𝐹 supp 0 ))𝑦 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |
79 | 9, 23, 78 | 3bitrd 293 |
1
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) |