| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ¬ 𝐷 ∈ Fin) |
| 2 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝐷 ⊆ ℂ) |
| 3 | 2 | sseld 3982 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → 𝑏 ∈ ℂ)) |
| 4 | | simprll 779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 ∈
(Poly‘ℂ)) |
| 5 | | plyf 26237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ (Poly‘ℂ)
→ 𝑝:ℂ⟶ℂ) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝:ℂ⟶ℂ) |
| 7 | 6 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 Fn ℂ) |
| 8 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑝 Fn ℂ) |
| 9 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎 ∈
(Poly‘ℂ)) |
| 10 | | plyf 26237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (Poly‘ℂ)
→ 𝑎:ℂ⟶ℂ) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎:ℂ⟶ℂ) |
| 12 | 11 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎 Fn ℂ) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑎 Fn ℂ) |
| 14 | | cnex 11236 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
| 15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ℂ ∈ V) |
| 16 | 2 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ ℂ) |
| 17 | | fnfvof 7714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 Fn ℂ ∧ 𝑎 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑏 ∈
ℂ)) → ((𝑝
∘f − 𝑎)‘𝑏) = ((𝑝‘𝑏) − (𝑎‘𝑏))) |
| 18 | 8, 13, 15, 16, 17 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ∘f − 𝑎)‘𝑏) = ((𝑝‘𝑏) − (𝑎‘𝑏))) |
| 19 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑝:ℂ⟶ℂ) |
| 20 | 19, 16 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝‘𝑏) ∈ ℂ) |
| 21 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ↾ 𝐷) = 𝐹) |
| 22 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑎 ↾ 𝐷) = 𝐹) |
| 23 | 21, 22 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
| 25 | 24 | fveq1d 6908 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ↾ 𝐷)‘𝑏) = ((𝑎 ↾ 𝐷)‘𝑏)) |
| 26 | | fvres 6925 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐷 → ((𝑝 ↾ 𝐷)‘𝑏) = (𝑝‘𝑏)) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ↾ 𝐷)‘𝑏) = (𝑝‘𝑏)) |
| 28 | | fvres 6925 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐷 → ((𝑎 ↾ 𝐷)‘𝑏) = (𝑎‘𝑏)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑎 ↾ 𝐷)‘𝑏) = (𝑎‘𝑏)) |
| 30 | 25, 27, 29 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝‘𝑏) = (𝑎‘𝑏)) |
| 31 | 20, 30 | subeq0bd 11689 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝‘𝑏) − (𝑎‘𝑏)) = 0) |
| 32 | 18, 31 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ∘f − 𝑎)‘𝑏) = 0) |
| 33 | 32 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → ((𝑝 ∘f − 𝑎)‘𝑏) = 0)) |
| 34 | 3, 33 | jcad 512 |
. . . . . . . . . . . 12
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → (𝑏 ∈ ℂ ∧ ((𝑝 ∘f − 𝑎)‘𝑏) = 0))) |
| 35 | | plysubcl 26261 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (Poly‘ℂ)
∧ 𝑎 ∈
(Poly‘ℂ)) → (𝑝 ∘f − 𝑎) ∈
(Poly‘ℂ)) |
| 36 | 4, 9, 35 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘f − 𝑎) ∈
(Poly‘ℂ)) |
| 37 | | plyf 26237 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘f −
𝑎) ∈
(Poly‘ℂ) → (𝑝 ∘f − 𝑎):ℂ⟶ℂ) |
| 38 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘f −
𝑎):ℂ⟶ℂ
→ (𝑝
∘f − 𝑎) Fn ℂ) |
| 39 | | fniniseg 7080 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘f −
𝑎) Fn ℂ → (𝑏 ∈ (◡(𝑝 ∘f − 𝑎) “ {0}) ↔ (𝑏 ∈ ℂ ∧ ((𝑝 ∘f −
𝑎)‘𝑏) = 0))) |
| 40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ (◡(𝑝 ∘f − 𝑎) “ {0}) ↔ (𝑏 ∈ ℂ ∧ ((𝑝 ∘f −
𝑎)‘𝑏) = 0))) |
| 41 | 34, 40 | sylibrd 259 |
. . . . . . . . . . 11
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → 𝑏 ∈ (◡(𝑝 ∘f − 𝑎) “
{0}))) |
| 42 | 41 | ssrdv 3989 |
. . . . . . . . . 10
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝐷 ⊆ (◡(𝑝 ∘f − 𝑎) “ {0})) |
| 43 | | ssfi 9213 |
. . . . . . . . . . 11
⊢ (((◡(𝑝 ∘f − 𝑎) “ {0}) ∈ Fin ∧
𝐷 ⊆ (◡(𝑝 ∘f − 𝑎) “ {0})) → 𝐷 ∈ Fin) |
| 44 | 43 | expcom 413 |
. . . . . . . . . 10
⊢ (𝐷 ⊆ (◡(𝑝 ∘f − 𝑎) “ {0}) → ((◡(𝑝 ∘f − 𝑎) “ {0}) ∈ Fin →
𝐷 ∈
Fin)) |
| 45 | 42, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ((◡(𝑝 ∘f − 𝑎) “ {0}) ∈ Fin →
𝐷 ∈
Fin)) |
| 46 | 1, 45 | mtod 198 |
. . . . . . . 8
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ¬ (◡(𝑝 ∘f − 𝑎) “ {0}) ∈
Fin) |
| 47 | | neqne 2948 |
. . . . . . . . . . 11
⊢ (¬
(𝑝 ∘f
− 𝑎) =
0𝑝 → (𝑝 ∘f − 𝑎) ≠
0𝑝) |
| 48 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (◡(𝑝 ∘f − 𝑎) “ {0}) = (◡(𝑝 ∘f − 𝑎) “ {0}) |
| 49 | 48 | fta1 26350 |
. . . . . . . . . . 11
⊢ (((𝑝 ∘f −
𝑎) ∈
(Poly‘ℂ) ∧ (𝑝 ∘f − 𝑎) ≠ 0𝑝)
→ ((◡(𝑝 ∘f − 𝑎) “ {0}) ∈ Fin ∧
(♯‘(◡(𝑝 ∘f − 𝑎) “ {0})) ≤
(deg‘(𝑝
∘f − 𝑎)))) |
| 50 | 36, 47, 49 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ ¬ (𝑝 ∘f − 𝑎) = 0𝑝)
→ ((◡(𝑝 ∘f − 𝑎) “ {0}) ∈ Fin ∧
(♯‘(◡(𝑝 ∘f − 𝑎) “ {0})) ≤
(deg‘(𝑝
∘f − 𝑎)))) |
| 51 | 50 | simpld 494 |
. . . . . . . . 9
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ ¬ (𝑝 ∘f − 𝑎) = 0𝑝)
→ (◡(𝑝 ∘f − 𝑎) “ {0}) ∈
Fin) |
| 52 | 51 | ex 412 |
. . . . . . . 8
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (¬ (𝑝 ∘f − 𝑎) = 0𝑝 →
(◡(𝑝 ∘f − 𝑎) “ {0}) ∈
Fin)) |
| 53 | 46, 52 | mt3d 148 |
. . . . . . 7
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘f − 𝑎) =
0𝑝) |
| 54 | | df-0p 25705 |
. . . . . . 7
⊢
0𝑝 = (ℂ × {0}) |
| 55 | 53, 54 | eqtrdi 2793 |
. . . . . 6
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘f − 𝑎) = (ℂ ×
{0})) |
| 56 | | ofsubeq0 12263 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝑝:ℂ⟶ℂ ∧ 𝑎:ℂ⟶ℂ) →
((𝑝 ∘f
− 𝑎) = (ℂ
× {0}) ↔ 𝑝 =
𝑎)) |
| 57 | 14, 6, 11, 56 | mp3an2i 1468 |
. . . . . 6
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ((𝑝 ∘f − 𝑎) = (ℂ × {0}) ↔
𝑝 = 𝑎)) |
| 58 | 55, 57 | mpbid 232 |
. . . . 5
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 = 𝑎) |
| 59 | 58 | ex 412 |
. . . 4
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
(((𝑝 ∈
(Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
| 60 | 59 | alrimivv 1928 |
. . 3
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∀𝑝∀𝑎(((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
| 61 | | eleq1w 2824 |
. . . . 5
⊢ (𝑝 = 𝑎 → (𝑝 ∈ (Poly‘ℂ) ↔ 𝑎 ∈
(Poly‘ℂ))) |
| 62 | | reseq1 5991 |
. . . . . 6
⊢ (𝑝 = 𝑎 → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
| 63 | 62 | eqeq1d 2739 |
. . . . 5
⊢ (𝑝 = 𝑎 → ((𝑝 ↾ 𝐷) = 𝐹 ↔ (𝑎 ↾ 𝐷) = 𝐹)) |
| 64 | 61, 63 | anbi12d 632 |
. . . 4
⊢ (𝑝 = 𝑎 → ((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ↔ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) |
| 65 | 64 | mo4 2566 |
. . 3
⊢
(∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ↔ ∀𝑝∀𝑎(((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
| 66 | 60, 65 | sylibr 234 |
. 2
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹)) |
| 67 | | plyssc 26239 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
| 68 | 67 | sseli 3979 |
. . . 4
⊢ (𝑝 ∈ (Poly‘𝑆) → 𝑝 ∈
(Poly‘ℂ)) |
| 69 | 68 | anim1i 615 |
. . 3
⊢ ((𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹) → (𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |
| 70 | 69 | moimi 2545 |
. 2
⊢
(∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) → ∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |
| 71 | 66, 70 | syl 17 |
1
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |