Step | Hyp | Ref
| Expression |
1 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ¬ 𝐷 ∈ Fin) |
2 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝐷 ⊆ ℂ) |
3 | 2 | sseld 3602 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → 𝑏 ∈ ℂ)) |
4 | | simprll 802 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 ∈
(Poly‘ℂ)) |
5 | | plyf 23954 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ (Poly‘ℂ)
→ 𝑝:ℂ⟶ℂ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝:ℂ⟶ℂ) |
7 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝:ℂ⟶ℂ →
𝑝 Fn
ℂ) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 Fn ℂ) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑝 Fn ℂ) |
10 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎 ∈
(Poly‘ℂ)) |
11 | | plyf 23954 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (Poly‘ℂ)
→ 𝑎:ℂ⟶ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎:ℂ⟶ℂ) |
13 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎:ℂ⟶ℂ →
𝑎 Fn
ℂ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑎 Fn ℂ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑎 Fn ℂ) |
16 | | cnex 10017 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ℂ ∈ V) |
18 | 2 | sselda 3603 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ ℂ) |
19 | | fnfvof 6911 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 Fn ℂ ∧ 𝑎 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑏 ∈
ℂ)) → ((𝑝
∘𝑓 − 𝑎)‘𝑏) = ((𝑝‘𝑏) − (𝑎‘𝑏))) |
20 | 9, 15, 17, 18, 19 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = ((𝑝‘𝑏) − (𝑎‘𝑏))) |
21 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → 𝑝:ℂ⟶ℂ) |
22 | 21, 18 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝‘𝑏) ∈ ℂ) |
23 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ↾ 𝐷) = 𝐹) |
24 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑎 ↾ 𝐷) = 𝐹) |
25 | 23, 24 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
27 | 26 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ↾ 𝐷)‘𝑏) = ((𝑎 ↾ 𝐷)‘𝑏)) |
28 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐷 → ((𝑝 ↾ 𝐷)‘𝑏) = (𝑝‘𝑏)) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ↾ 𝐷)‘𝑏) = (𝑝‘𝑏)) |
30 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐷 → ((𝑎 ↾ 𝐷)‘𝑏) = (𝑎‘𝑏)) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑎 ↾ 𝐷)‘𝑏) = (𝑎‘𝑏)) |
32 | 27, 29, 31 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → (𝑝‘𝑏) = (𝑎‘𝑏)) |
33 | 22, 32 | subeq0bd 10456 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝‘𝑏) − (𝑎‘𝑏)) = 0) |
34 | 20, 33 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ 𝑏 ∈ 𝐷) → ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = 0) |
35 | 34 | ex 450 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = 0)) |
36 | 3, 35 | jcad 555 |
. . . . . . . . . . . 12
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → (𝑏 ∈ ℂ ∧ ((𝑝 ∘𝑓 − 𝑎)‘𝑏) = 0))) |
37 | | plysubcl 23978 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (Poly‘ℂ)
∧ 𝑎 ∈
(Poly‘ℂ)) → (𝑝 ∘𝑓 − 𝑎) ∈
(Poly‘ℂ)) |
38 | 4, 10, 37 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘𝑓 − 𝑎) ∈
(Poly‘ℂ)) |
39 | | plyf 23954 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘𝑓
− 𝑎) ∈
(Poly‘ℂ) → (𝑝 ∘𝑓 − 𝑎):ℂ⟶ℂ) |
40 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘𝑓
− 𝑎):ℂ⟶ℂ → (𝑝 ∘𝑓
− 𝑎) Fn
ℂ) |
41 | | fniniseg 6338 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∘𝑓
− 𝑎) Fn ℂ
→ (𝑏 ∈ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ↔ (𝑏 ∈ ℂ ∧ ((𝑝 ∘𝑓
− 𝑎)‘𝑏) = 0))) |
42 | 38, 39, 40, 41 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ↔ (𝑏 ∈ ℂ ∧ ((𝑝 ∘𝑓
− 𝑎)‘𝑏) = 0))) |
43 | 36, 42 | sylibrd 249 |
. . . . . . . . . . 11
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑏 ∈ 𝐷 → 𝑏 ∈ (◡(𝑝 ∘𝑓 − 𝑎) “
{0}))) |
44 | 43 | ssrdv 3609 |
. . . . . . . . . 10
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝐷 ⊆ (◡(𝑝 ∘𝑓 − 𝑎) “ {0})) |
45 | | ssfi 8180 |
. . . . . . . . . . 11
⊢ (((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin ∧
𝐷 ⊆ (◡(𝑝 ∘𝑓 − 𝑎) “ {0})) → 𝐷 ∈ Fin) |
46 | 45 | expcom 451 |
. . . . . . . . . 10
⊢ (𝐷 ⊆ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) → ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin →
𝐷 ∈
Fin)) |
47 | 44, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin →
𝐷 ∈
Fin)) |
48 | 1, 47 | mtod 189 |
. . . . . . . 8
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ¬ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈
Fin) |
49 | | df-ne 2795 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∘𝑓
− 𝑎) ≠
0𝑝 ↔ ¬ (𝑝 ∘𝑓 − 𝑎) =
0𝑝) |
50 | 49 | biimpri 218 |
. . . . . . . . . . 11
⊢ (¬
(𝑝
∘𝑓 − 𝑎) = 0𝑝 → (𝑝 ∘𝑓
− 𝑎) ≠
0𝑝) |
51 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) = (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) |
52 | 51 | fta1 24063 |
. . . . . . . . . . 11
⊢ (((𝑝 ∘𝑓
− 𝑎) ∈
(Poly‘ℂ) ∧ (𝑝 ∘𝑓 − 𝑎) ≠ 0𝑝)
→ ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin ∧
(#‘(◡(𝑝 ∘𝑓 − 𝑎) “ {0})) ≤
(deg‘(𝑝
∘𝑓 − 𝑎)))) |
53 | 38, 50, 52 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ ¬ (𝑝 ∘𝑓 − 𝑎) = 0𝑝)
→ ((◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈ Fin ∧
(#‘(◡(𝑝 ∘𝑓 − 𝑎) “ {0})) ≤
(deg‘(𝑝
∘𝑓 − 𝑎)))) |
54 | 53 | simpld 475 |
. . . . . . . . 9
⊢ ((((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) ∧ ¬ (𝑝 ∘𝑓 − 𝑎) = 0𝑝)
→ (◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈
Fin) |
55 | 54 | ex 450 |
. . . . . . . 8
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (¬ (𝑝 ∘𝑓 − 𝑎) = 0𝑝 →
(◡(𝑝 ∘𝑓 − 𝑎) “ {0}) ∈
Fin)) |
56 | 48, 55 | mt3d 140 |
. . . . . . 7
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘𝑓 − 𝑎) =
0𝑝) |
57 | | df-0p 23437 |
. . . . . . 7
⊢
0𝑝 = (ℂ × {0}) |
58 | 56, 57 | syl6eq 2672 |
. . . . . 6
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → (𝑝 ∘𝑓 − 𝑎) = (ℂ ×
{0})) |
59 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ℂ ∈
V) |
60 | | ofsubeq0 11017 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝑝:ℂ⟶ℂ ∧ 𝑎:ℂ⟶ℂ) →
((𝑝
∘𝑓 − 𝑎) = (ℂ × {0}) ↔ 𝑝 = 𝑎)) |
61 | 59, 6, 12, 60 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → ((𝑝 ∘𝑓 − 𝑎) = (ℂ × {0}) ↔
𝑝 = 𝑎)) |
62 | 58, 61 | mpbid 222 |
. . . . 5
⊢ (((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) ∧ ((𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) → 𝑝 = 𝑎) |
63 | 62 | ex 450 |
. . . 4
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
(((𝑝 ∈
(Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
64 | 63 | alrimivv 1856 |
. . 3
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∀𝑝∀𝑎(((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
65 | | eleq1 2689 |
. . . . 5
⊢ (𝑝 = 𝑎 → (𝑝 ∈ (Poly‘ℂ) ↔ 𝑎 ∈
(Poly‘ℂ))) |
66 | | reseq1 5390 |
. . . . . 6
⊢ (𝑝 = 𝑎 → (𝑝 ↾ 𝐷) = (𝑎 ↾ 𝐷)) |
67 | 66 | eqeq1d 2624 |
. . . . 5
⊢ (𝑝 = 𝑎 → ((𝑝 ↾ 𝐷) = 𝐹 ↔ (𝑎 ↾ 𝐷) = 𝐹)) |
68 | 65, 67 | anbi12d 747 |
. . . 4
⊢ (𝑝 = 𝑎 → ((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ↔ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹))) |
69 | 68 | mo4 2517 |
. . 3
⊢
(∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) ↔ ∀𝑝∀𝑎(((𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹) ∧ (𝑎 ∈ (Poly‘ℂ) ∧ (𝑎 ↾ 𝐷) = 𝐹)) → 𝑝 = 𝑎)) |
70 | 64, 69 | sylibr 224 |
. 2
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹)) |
71 | | plyssc 23956 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
72 | 71 | sseli 3599 |
. . . 4
⊢ (𝑝 ∈ (Poly‘𝑆) → 𝑝 ∈
(Poly‘ℂ)) |
73 | 72 | anim1i 592 |
. . 3
⊢ ((𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹) → (𝑝 ∈ (Poly‘ℂ) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |
74 | 73 | moimi 2520 |
. 2
⊢
(∃*𝑝(𝑝 ∈ (Poly‘ℂ)
∧ (𝑝 ↾ 𝐷) = 𝐹) → ∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |
75 | 70, 74 | syl 17 |
1
⊢ ((𝐷 ⊆ ℂ ∧ ¬
𝐷 ∈ Fin) →
∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) |