| Step | Hyp | Ref
| Expression |
| 1 | | mdegcl.d |
. . 3
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
| 2 | | mdegcl.p |
. . 3
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
| 3 | | mdegcl.b |
. . 3
⊢ 𝐵 = (Base‘𝑃) |
| 4 | | eqid 2737 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 5 | | eqid 2737 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin} |
| 6 | | eqid 2737 |
. . 3
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
| 7 | 1, 2, 3, 4, 5, 6 | mdegval 26102 |
. 2
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, <
)) |
| 8 | | supeq1 9485 |
. . . 4
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) = ∅ → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) =
sup(∅, ℝ*, < )) |
| 9 | 8 | eleq1d 2826 |
. . 3
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) = ∅ → (sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
(ℕ0 ∪ {-∞}) ↔ sup(∅, ℝ*,
< ) ∈ (ℕ0 ∪ {-∞}))) |
| 10 | | imassrn 6089 |
. . . . . . 7
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ ran (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
| 11 | 5, 6 | tdeglem1 26097 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0 |
| 12 | | frn 6743 |
. . . . . . . 8
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0 → ran (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) ⊆
ℕ0) |
| 13 | 11, 12 | mp1i 13 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → ran (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) ⊆
ℕ0) |
| 14 | 10, 13 | sstrid 3995 |
. . . . . 6
⊢ (𝐹 ∈ 𝐵 → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆
ℕ0) |
| 15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆
ℕ0) |
| 16 | | ssun1 4178 |
. . . . 5
⊢
ℕ0 ⊆ (ℕ0 ∪
{-∞}) |
| 17 | 15, 16 | sstrdi 3996 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ (ℕ0 ∪
{-∞})) |
| 18 | | ffun 6739 |
. . . . . . . 8
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0 → Fun (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))) |
| 19 | 11, 18 | mp1i 13 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → Fun (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))) |
| 20 | | id 22 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵) |
| 21 | 2, 3, 4, 20 | mplelsfi 22015 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → 𝐹 finSupp (0g‘𝑅)) |
| 22 | 21 | fsuppimpd 9409 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → (𝐹 supp (0g‘𝑅)) ∈ Fin) |
| 23 | | imafi 9353 |
. . . . . . 7
⊢ ((Fun
(𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) ∧ (𝐹 supp (0g‘𝑅)) ∈ Fin) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin) |
| 24 | 19, 22, 23 | syl2anc 584 |
. . . . . 6
⊢ (𝐹 ∈ 𝐵 → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin) |
| 25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin) |
| 26 | | simpr 484 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) |
| 27 | | nn0ssre 12530 |
. . . . . . 7
⊢
ℕ0 ⊆ ℝ |
| 28 | | ressxr 11305 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
| 29 | 27, 28 | sstri 3993 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ* |
| 30 | 15, 29 | sstrdi 3996 |
. . . . 5
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆
ℝ*) |
| 31 | | xrltso 13183 |
. . . . . 6
⊢ < Or
ℝ* |
| 32 | | fisupcl 9509 |
. . . . . 6
⊢ (( <
Or ℝ* ∧ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅ ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ ℝ*)) →
sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅)))) |
| 33 | 31, 32 | mpan 690 |
. . . . 5
⊢ ((((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ∈ Fin ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅ ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ⊆ ℝ*) →
sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅)))) |
| 34 | 25, 26, 30, 33 | syl3anc 1373 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅)))) |
| 35 | 17, 34 | sseldd 3984 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))) ≠ ∅) → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
(ℕ0 ∪ {-∞})) |
| 36 | | xrsup0 13365 |
. . . . 5
⊢
sup(∅, ℝ*, < ) = -∞ |
| 37 | | ssun2 4179 |
. . . . . 6
⊢
{-∞} ⊆ (ℕ0 ∪
{-∞}) |
| 38 | | mnfxr 11318 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
| 39 | 38 | elexi 3503 |
. . . . . . 7
⊢ -∞
∈ V |
| 40 | 39 | snid 4662 |
. . . . . 6
⊢ -∞
∈ {-∞} |
| 41 | 37, 40 | sselii 3980 |
. . . . 5
⊢ -∞
∈ (ℕ0 ∪ {-∞}) |
| 42 | 36, 41 | eqeltri 2837 |
. . . 4
⊢
sup(∅, ℝ*, < ) ∈ (ℕ0
∪ {-∞}) |
| 43 | 42 | a1i 11 |
. . 3
⊢ (𝐹 ∈ 𝐵 → sup(∅, ℝ*,
< ) ∈ (ℕ0 ∪ {-∞})) |
| 44 | 9, 35, 43 | pm2.61ne 3027 |
. 2
⊢ (𝐹 ∈ 𝐵 → sup(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) “ (𝐹 supp (0g‘𝑅))), ℝ*, < ) ∈
(ℕ0 ∪ {-∞})) |
| 45 | 7, 44 | eqeltrd 2841 |
1
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪
{-∞})) |