Step | Hyp | Ref
| Expression |
1 | | mdegcl.d |
. . 3
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
2 | | mdegcl.p |
. . 3
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
3 | | mdegcl.b |
. . 3
⊢ 𝐵 = (Base‘𝑃) |
4 | | eqid 2778 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | eqid 2778 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
6 | | eqid 2778 |
. . 3
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
7 | 1, 2, 3, 4, 5, 6 | mdegval 24260 |
. 2
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, <
)) |
8 | | supeq1 8639 |
. . . 4
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) = ∅ → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) =
sup(∅, ℝ*, < )) |
9 | 8 | eleq1d 2844 |
. . 3
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) = ∅ → (sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
(ℕ0 ∪ {-∞}) ↔ sup(∅, ℝ*,
< ) ∈ (ℕ0 ∪ {-∞}))) |
10 | | imassrn 5731 |
. . . . . . 7
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ ran (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
11 | 2, 3 | mplrcl 19886 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) |
12 | 5, 6 | tdeglem1 24255 |
. . . . . . . 8
⊢ (𝐼 ∈ V → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
13 | | frn 6297 |
. . . . . . . 8
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0 → ran (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) ⊆
ℕ0) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → ran (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) ⊆
ℕ0) |
15 | 10, 14 | syl5ss 3832 |
. . . . . 6
⊢ (𝐹 ∈ 𝐵 → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆
ℕ0) |
16 | 15 | adantr 474 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆
ℕ0) |
17 | | ssun1 3999 |
. . . . 5
⊢
ℕ0 ⊆ (ℕ0 ∪
{-∞}) |
18 | 16, 17 | syl6ss 3833 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ (ℕ0 ∪
{-∞})) |
19 | | ffun 6294 |
. . . . . . . 8
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0 → Fun (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))) |
20 | 11, 12, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → Fun (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))) |
21 | | id 22 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵) |
22 | | reldmmpl 19824 |
. . . . . . . . . . 11
⊢ Rel dom
mPoly |
23 | 22, 2, 3 | elbasov 16317 |
. . . . . . . . . 10
⊢ (𝐹 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
24 | 23 | simprd 491 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐵 → 𝑅 ∈ V) |
25 | 2, 3, 4, 21, 24 | mplelsfi 19887 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → 𝐹 finSupp (0g‘𝑅)) |
26 | 25 | fsuppimpd 8570 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → (𝐹 supp (0g‘𝑅)) ∈ Fin) |
27 | | imafi 8547 |
. . . . . . 7
⊢ ((Fun
(𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) ∧ (𝐹 supp (0g‘𝑅)) ∈ Fin) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin) |
28 | 20, 26, 27 | syl2anc 579 |
. . . . . 6
⊢ (𝐹 ∈ 𝐵 → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin) |
29 | 28 | adantr 474 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin) |
30 | | simpr 479 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) |
31 | | nn0ssre 11646 |
. . . . . . 7
⊢
ℕ0 ⊆ ℝ |
32 | | ressxr 10420 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
33 | 31, 32 | sstri 3830 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ* |
34 | 16, 33 | syl6ss 3833 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆
ℝ*) |
35 | | xrltso 12284 |
. . . . . 6
⊢ < Or
ℝ* |
36 | | fisupcl 8663 |
. . . . . 6
⊢ (( <
Or ℝ* ∧ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅ ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ ℝ*)) →
sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅)))) |
37 | 35, 36 | mpan 680 |
. . . . 5
⊢ ((((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅ ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ ℝ*) →
sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅)))) |
38 | 29, 30, 34, 37 | syl3anc 1439 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅)))) |
39 | 18, 38 | sseldd 3822 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
(ℕ0 ∪ {-∞})) |
40 | | xrsup0 12465 |
. . . . 5
⊢
sup(∅, ℝ*, < ) = -∞ |
41 | | ssun2 4000 |
. . . . . 6
⊢
{-∞} ⊆ (ℕ0 ∪
{-∞}) |
42 | | mnfxr 10434 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
43 | 42 | elexi 3415 |
. . . . . . 7
⊢ -∞
∈ V |
44 | 43 | snid 4430 |
. . . . . 6
⊢ -∞
∈ {-∞} |
45 | 41, 44 | sselii 3818 |
. . . . 5
⊢ -∞
∈ (ℕ0 ∪ {-∞}) |
46 | 40, 45 | eqeltri 2855 |
. . . 4
⊢
sup(∅, ℝ*, < ) ∈ (ℕ0
∪ {-∞}) |
47 | 46 | a1i 11 |
. . 3
⊢ (𝐹 ∈ 𝐵 → sup(∅, ℝ*,
< ) ∈ (ℕ0 ∪ {-∞})) |
48 | 9, 39, 47 | pm2.61ne 3055 |
. 2
⊢ (𝐹 ∈ 𝐵 → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
(ℕ0 ∪ {-∞})) |
49 | 7, 48 | eqeltrd 2859 |
1
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪
{-∞})) |