Step | Hyp | Ref
| Expression |
1 | | mdegle0.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
2 | | 0xr 10403 |
. . 3
⊢ 0 ∈
ℝ* |
3 | | mdegaddle.d |
. . . 4
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
4 | | mdegaddle.y |
. . . 4
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
5 | | mdegle0.b |
. . . 4
⊢ 𝐵 = (Base‘𝑌) |
6 | | eqid 2825 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
7 | | eqid 2825 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
8 | | eqid 2825 |
. . . 4
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
9 | 3, 4, 5, 6, 7, 8 | mdegleb 24223 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 0 ∈ ℝ*) →
((𝐷‘𝐹) ≤ 0 ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)))) |
10 | 1, 2, 9 | sylancl 580 |
. 2
⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)))) |
11 | | mdegaddle.i |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
12 | 7, 8 | tdeglem1 24217 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
14 | 13 | ffvelrnda 6608 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈
ℕ0) |
15 | | nn0re 11628 |
. . . . . . . . 9
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℝ) |
16 | | nn0ge0 11645 |
. . . . . . . . 9
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → 0 ≤
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥)) |
17 | 15, 16 | jca 507 |
. . . . . . . 8
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) |
18 | | ne0gt0 10461 |
. . . . . . . 8
⊢ ((((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥)) → (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ 0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) |
19 | 14, 17, 18 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ 0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) |
20 | 7, 8 | tdeglem4 24219 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) = 0 ↔ 𝑥 = (𝐼 × {0}))) |
21 | 11, 20 | sylan 575 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) = 0 ↔ 𝑥 = (𝐼 × {0}))) |
22 | 21 | necon3abid 3035 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ ¬ 𝑥 = (𝐼 × {0}))) |
23 | 19, 22 | bitr3d 273 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (0 <
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ↔ ¬ 𝑥 = (𝐼 × {0}))) |
24 | 23 | imbi1d 333 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((0
< ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
25 | | eqeq2 2836 |
. . . . . . . 8
⊢ ((𝐹‘(𝐼 × {0})) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
26 | 25 | bibi1d 335 |
. . . . . . 7
⊢ ((𝐹‘(𝐼 × {0})) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → (((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) ↔ ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))) |
27 | | eqeq2 2836 |
. . . . . . . 8
⊢
((0g‘𝑅) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
28 | 27 | bibi1d 335 |
. . . . . . 7
⊢
((0g‘𝑅) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → (((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) ↔ ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))) |
29 | | fveq2 6433 |
. . . . . . . . 9
⊢ (𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (𝐹‘(𝐼 × {0}))) |
30 | | pm2.24 122 |
. . . . . . . . 9
⊢ (𝑥 = (𝐼 × {0}) → (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) |
31 | 29, 30 | 2thd 257 |
. . . . . . . 8
⊢ (𝑥 = (𝐼 × {0}) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
32 | 31 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = (𝐼 × {0})) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
33 | | biimt 352 |
. . . . . . . 8
⊢ (¬
𝑥 = (𝐼 × {0}) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
34 | 33 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑥 = (𝐼 × {0})) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
35 | 26, 28, 32, 34 | ifbothda 4343 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
36 | 35 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
37 | 24, 36 | bitr4d 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((0
< ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
38 | 37 | ralbidva 3194 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
39 | | eqid 2825 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
40 | 4, 39, 5, 7, 1 | mplelf 19794 |
. . . . . 6
⊢ (𝜑 → 𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
41 | 40 | feqmptd 6496 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥))) |
42 | | mdegle0.a |
. . . . . 6
⊢ 𝐴 = (algSc‘𝑌) |
43 | | mdegaddle.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
44 | 7 | psrbag0 19854 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
45 | 11, 44 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐼 × {0}) ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
46 | 40, 45 | ffvelrnd 6609 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝐼 × {0})) ∈ (Base‘𝑅)) |
47 | 4, 7, 6, 39, 42, 11, 43, 46 | mplascl 19856 |
. . . . 5
⊢ (𝜑 → (𝐴‘(𝐹‘(𝐼 × {0}))) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
48 | 41, 47 | eqeq12d 2840 |
. . . 4
⊢ (𝜑 → (𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))) ↔ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))) |
49 | | fvex 6446 |
. . . . . 6
⊢ (𝐹‘𝑥) ∈ V |
50 | 49 | rgenw 3133 |
. . . . 5
⊢
∀𝑥 ∈
{𝑎 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) ∈ V |
51 | | mpteqb 6546 |
. . . . 5
⊢
(∀𝑥 ∈
{𝑎 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) ∈ V → ((𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
52 | 50, 51 | mp1i 13 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
53 | 48, 52 | bitrd 271 |
. . 3
⊢ (𝜑 → (𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
54 | 38, 53 | bitr4d 274 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))))) |
55 | 10, 54 | bitrd 271 |
1
⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))))) |