Step | Hyp | Ref
| Expression |
1 | | mdegle0.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
2 | | 0xr 10676 |
. . 3
⊢ 0 ∈
ℝ* |
3 | | mdegaddle.d |
. . . 4
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
4 | | mdegaddle.y |
. . . 4
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
5 | | mdegle0.b |
. . . 4
⊢ 𝐵 = (Base‘𝑌) |
6 | | eqid 2818 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
7 | | eqid 2818 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin} |
8 | | eqid 2818 |
. . . 4
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
9 | 3, 4, 5, 6, 7, 8 | mdegleb 24585 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 0 ∈ ℝ*) →
((𝐷‘𝐹) ≤ 0 ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)))) |
10 | 1, 2, 9 | sylancl 586 |
. 2
⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)))) |
11 | | mdegaddle.i |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
12 | 7, 8 | tdeglem1 24579 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
14 | 13 | ffvelrnda 6843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈
ℕ0) |
15 | | nn0re 11894 |
. . . . . . . . 9
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℝ) |
16 | | nn0ge0 11910 |
. . . . . . . . 9
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → 0 ≤
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥)) |
17 | 15, 16 | jca 512 |
. . . . . . . 8
⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) |
18 | | ne0gt0 10733 |
. . . . . . . 8
⊢ ((((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥)) → (((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ 0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) |
19 | 14, 17, 18 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ 0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) |
20 | 7, 8 | tdeglem4 24581 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) = 0 ↔ 𝑥 = (𝐼 × {0}))) |
21 | 11, 20 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) = 0 ↔ 𝑥 = (𝐼 × {0}))) |
22 | 21 | necon3abid 3049 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ ¬ 𝑥 = (𝐼 × {0}))) |
23 | 19, 22 | bitr3d 282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (0 <
((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) ↔ ¬ 𝑥 = (𝐼 × {0}))) |
24 | 23 | imbi1d 343 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((0
< ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
25 | | eqeq2 2830 |
. . . . . . . 8
⊢ ((𝐹‘(𝐼 × {0})) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
26 | 25 | bibi1d 345 |
. . . . . . 7
⊢ ((𝐹‘(𝐼 × {0})) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → (((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) ↔ ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))) |
27 | | eqeq2 2830 |
. . . . . . . 8
⊢
((0g‘𝑅) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
28 | 27 | bibi1d 345 |
. . . . . . 7
⊢
((0g‘𝑅) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → (((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) ↔ ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))) |
29 | | fveq2 6663 |
. . . . . . . . 9
⊢ (𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (𝐹‘(𝐼 × {0}))) |
30 | | pm2.24 124 |
. . . . . . . . 9
⊢ (𝑥 = (𝐼 × {0}) → (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) |
31 | 29, 30 | 2thd 266 |
. . . . . . . 8
⊢ (𝑥 = (𝐼 × {0}) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
32 | 31 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = (𝐼 × {0})) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
33 | | biimt 362 |
. . . . . . . 8
⊢ (¬
𝑥 = (𝐼 × {0}) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
34 | 33 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑥 = (𝐼 × {0})) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
35 | 26, 28, 32, 34 | ifbothda 4500 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
36 | 35 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))) |
37 | 24, 36 | bitr4d 283 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((0
< ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
38 | 37 | ralbidva 3193 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
39 | | eqid 2818 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
40 | 4, 39, 5, 7, 1 | mplelf 20141 |
. . . . . 6
⊢ (𝜑 → 𝐹:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
41 | 40 | feqmptd 6726 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥))) |
42 | | mdegle0.a |
. . . . . 6
⊢ 𝐴 = (algSc‘𝑌) |
43 | | mdegaddle.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
44 | 7 | psrbag0 20202 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
45 | 11, 44 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐼 × {0}) ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
46 | 40, 45 | ffvelrnd 6844 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝐼 × {0})) ∈ (Base‘𝑅)) |
47 | 4, 7, 6, 39, 42, 11, 43, 46 | mplascl 20204 |
. . . . 5
⊢ (𝜑 → (𝐴‘(𝐹‘(𝐼 × {0}))) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
48 | 41, 47 | eqeq12d 2834 |
. . . 4
⊢ (𝜑 → (𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))) ↔ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))) |
49 | | fvex 6676 |
. . . . . 6
⊢ (𝐹‘𝑥) ∈ V |
50 | 49 | rgenw 3147 |
. . . . 5
⊢
∀𝑥 ∈
{𝑎 ∈
(ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) ∈ V |
51 | | mpteqb 6779 |
. . . . 5
⊢
(∀𝑥 ∈
{𝑎 ∈
(ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) ∈ V → ((𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
52 | 50, 51 | mp1i 13 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
53 | 48, 52 | bitrd 280 |
. . 3
⊢ (𝜑 → (𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))) |
54 | 38, 53 | bitr4d 283 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))))) |
55 | 10, 54 | bitrd 280 |
1
⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))))) |