Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ¬ 𝐷 ∈ Fin) |
2 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝐷 ⊆ ℂ) |
3 | 2 | sseld 3567 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → 𝑏 ∈ ℂ)) |
4 | | simprll 798 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 ∈
(Poly‘ℂ)) |
5 | | plyf 23758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ (Poly‘ℂ)
→ 𝑝:ℂ⟶ℂ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝:ℂ⟶ℂ) |
7 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝:ℂ⟶ℂ →
𝑝 Fn
ℂ) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 Fn ℂ) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑝 Fn ℂ) |
10 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎 ∈
(Poly‘ℂ)) |
11 | | plyf 23758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (Poly‘ℂ)
→ 𝑎:ℂ⟶ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎:ℂ⟶ℂ) |
13 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎:ℂ⟶ℂ →
𝑎 Fn
ℂ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎 Fn ℂ) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑎 Fn ℂ) |
16 | | cnex 9896 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ℂ ∈ V) |
18 | 2 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ ℂ) |
19 | | fnfvof 6809 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 Fn ℂ ∧ 𝑎 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑏 ∈
ℂ)) → ((𝑝
∘𝑓 − 𝑎)‘𝑏) = ((𝑝‘𝑏) − (𝑎‘𝑏))) |
20 | 9, 15, 17, 18, 19 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = ((𝑝‘𝑏) − (𝑎‘𝑏))) |
21 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑝:ℂ⟶ℂ) |
22 | 21, 18 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝‘𝑏) ∈ ℂ) |
23 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ↾ 𝐷) = 𝐹) |
24 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑎 ↾ 𝐷) = 𝐹) |
25 | 23, 24 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
27 | 26 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ↾ 𝐷)‘𝑏) = ((𝑎 ↾ 𝐷)‘𝑏)) |
28 | | fvres 6117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐷 → ((𝑝 ↾ 𝐷)‘𝑏) = (𝑝‘𝑏)) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ↾ 𝐷)‘𝑏) = (𝑝‘𝑏)) |
30 | | fvres 6117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐷 → ((𝑎 ↾ 𝐷)‘𝑏) = (𝑎‘𝑏)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑎 ↾ 𝐷)‘𝑏) = (𝑎‘𝑏)) |
32 | 27, 29, 31 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝‘𝑏) = (𝑎‘𝑏)) |
33 | 22, 32 | subeq0bd 10335 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝‘𝑏) − (𝑎‘𝑏)) = 0) |
34 | 20, 33 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = 0) |
35 | 34 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = 0)) |
36 | 3, 35 | jcad 554 |
. . . . . . . . . . . 12
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → (𝑏 ∈ ℂ ∧ ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = 0))) |
37 | | plysubcl 23782 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (Poly‘ℂ)
∧ 𝑎 ∈
(Poly‘ℂ)) → (𝑝 ∘𝑓 − 𝑎) ∈
(Poly‘ℂ)) |
38 | 4, 10, 37 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘𝑓 − 𝑎) ∈
(Poly‘ℂ)) |
39 | | plyf 23758 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘𝑓
− 𝑎) ∈
(Poly‘ℂ) → (𝑝 ∘𝑓 − 𝑎):ℂ⟶ℂ) |
40 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘𝑓
− 𝑎):ℂ⟶ℂ → (𝑝 ∘𝑓
− 𝑎) Fn
ℂ) |
41 | | fniniseg 6246 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘𝑓
− 𝑎) Fn ℂ
→ (𝑏 ∈ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ↔ (𝑏 ∈ ℂ ∧ ((𝑝 ∘𝑓
− 𝑎)‘𝑏) = 0))) |
42 | 38, 39, 40, 41 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ↔ (𝑏 ∈ ℂ ∧ ((𝑝 ∘𝑓
− 𝑎)‘𝑏) = 0))) |
43 | 36, 42 | sylibrd 248 |
. . . . . . . . . . 11
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → 𝑏 ∈ (◡(𝑝 ∘𝑓 − 𝑎) “
{0}))) |
44 | 43 | ssrdv 3574 |
. . . . . . . . . 10
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝐷 ⊆ (◡(𝑝 ∘𝑓 − 𝑎) “ {0})) |
45 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ (((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin ∧
𝐷 ⊆ (◡(𝑝 ∘𝑓 − 𝑎) “ {0})) → 𝐷 ∈ Fin) |
46 | 45 | expcom 450 |
. . . . . . . . . 10
⊢ (𝐷 ⊆ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) → ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin →
𝐷 ∈
Fin)) |
47 | 44, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin →
𝐷 ∈
Fin)) |
48 | 1, 47 | mtod 188 |
. . . . . . . 8
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ¬ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈
Fin) |
49 | | df-ne 2782 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∘𝑓
− 𝑎) ≠
0𝑝 ↔ ¬ (𝑝 ∘𝑓 − 𝑎) =
0𝑝) |
50 | 49 | biimpri 217 |
. . . . . . . . . . 11
⊢ (¬
(𝑝
∘𝑓 − 𝑎) = 0𝑝 → (𝑝 ∘𝑓
− 𝑎) ≠
0𝑝) |
51 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) = (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) |
52 | 51 | fta1 23867 |
. . . . . . . . . . 11
⊢ (((𝑝 ∘𝑓
− 𝑎) ∈
(Poly‘ℂ) ∧ (𝑝 ∘𝑓 − 𝑎) ≠ 0𝑝)
→ ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin ∧
(#‘(◡(𝑝 ∘𝑓 − 𝑎) “ {0})) ≤
(deg‘(𝑝
∘𝑓 − 𝑎)))) |
53 | 38, 50, 52 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ ¬ (𝑝 ∘𝑓 − 𝑎) = 0𝑝)
→ ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin ∧
(#‘(◡(𝑝 ∘𝑓 − 𝑎) “ {0})) ≤
(deg‘(𝑝
∘𝑓 − 𝑎)))) |
54 | 53 | simpld 474 |
. . . . . . . . 9
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ ¬ (𝑝 ∘𝑓 − 𝑎) = 0𝑝)
→ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈
Fin) |
55 | 54 | ex 449 |
. . . . . . . 8
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (¬ (𝑝 ∘𝑓 − 𝑎) = 0𝑝 →
(◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈
Fin)) |
56 | 48, 55 | mt3d 139 |
. . . . . . 7
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘𝑓 − 𝑎) =
0𝑝) |
57 | | df-0p 23243 |
. . . . . . 7
⊢
0𝑝 = (ℂ × {0}) |
58 | 56, 57 | syl6eq 2660 |
. . . . . 6
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘𝑓 − 𝑎) = (ℂ ×
{0})) |
59 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ℂ ∈
V) |
60 | | ofsubeq0 10894 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝑝:ℂ⟶ℂ ∧ 𝑎:ℂ⟶ℂ) →
((𝑝
∘𝑓 − 𝑎) = (ℂ × {0}) ↔ 𝑝 = 𝑎)) |
61 | 59, 6, 12, 60 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ((𝑝 ∘𝑓 − 𝑎) = (ℂ × {0}) ↔
𝑝 = 𝑎)) |
62 | 58, 61 | mpbid 221 |
. . . . 5
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 = 𝑎) |
63 | 62 | ex 449 |
. . . 4
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
(((𝑝 ∈
(Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
64 | 63 | alrimivv 1843 |
. . 3
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∀𝑝∀𝑎(((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
65 | | eleq1 2676 |
. . . . 5
⊢ (𝑝 = 𝑎 → (𝑝 ∈ (Poly‘ℂ) ↔ 𝑎 ∈
(Poly‘ℂ))) |
66 | | reseq1 5311 |
. . . . . 6
⊢ (𝑝 = 𝑎 → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
67 | 66 | eqeq1d 2612 |
. . . . 5
⊢ (𝑝 = 𝑎 → ((𝑝 ↾ 𝐷) = 𝐹 ↔ (𝑎 ↾ 𝐷) = 𝐹)) |
68 | 65, 67 | anbi12d 743 |
. . . 4
⊢ (𝑝 = 𝑎 → ((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ↔ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) |
69 | 68 | mo4 2505 |
. . 3
⊢
(∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ↔ ∀𝑝∀𝑎(((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
70 | 64, 69 | sylibr 223 |
. 2
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹)) |
71 | | plyssc 23760 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
72 | 71 | sseli 3564 |
. . . 4
⊢ (𝑝 ∈ (Poly‘𝑆) → 𝑝 ∈
(Poly‘ℂ)) |
73 | 72 | anim1i 590 |
. . 3
⊢ ((𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹) → (𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |
74 | 73 | moimi 2508 |
. 2
⊢
(∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) → ∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |
75 | 70, 74 | syl 17 |
1
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |