Metamath Proof Explorer

Theorem plyexmo

Description: An infinite set of values can be extended to a polynomial in at most one way. (Contributed by Stefan O'Rear, 14-Nov-2014)

Ref Expression
Assertion plyexmo ${⊢}\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\to {\exists }^{*}{p}\phantom{\rule{.4em}{0ex}}\left({p}\in \mathrm{Poly}\left({S}\right)\wedge {{p}↾}_{{D}}={F}\right)$

Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to ¬{D}\in \mathrm{Fin}$
2 simpll ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {D}\subseteq ℂ$
3 2 sseld ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({b}\in {D}\to {b}\in ℂ\right)$
4 simprll ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}\in \mathrm{Poly}\left(ℂ\right)$
5 plyf ${⊢}{p}\in \mathrm{Poly}\left(ℂ\right)\to {p}:ℂ⟶ℂ$
6 4 5 syl ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}:ℂ⟶ℂ$
7 6 ffnd ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}Fnℂ$
8 7 adantr ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {p}Fnℂ$
9 simprrl ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {a}\in \mathrm{Poly}\left(ℂ\right)$
10 plyf ${⊢}{a}\in \mathrm{Poly}\left(ℂ\right)\to {a}:ℂ⟶ℂ$
11 9 10 syl ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {a}:ℂ⟶ℂ$
12 11 ffnd ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {a}Fnℂ$
13 12 adantr ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {a}Fnℂ$
14 cnex ${⊢}ℂ\in \mathrm{V}$
15 14 a1i ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to ℂ\in \mathrm{V}$
16 2 sselda ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {b}\in ℂ$
17 fnfvof ${⊢}\left(\left({p}Fnℂ\wedge {a}Fnℂ\right)\wedge \left(ℂ\in \mathrm{V}\wedge {b}\in ℂ\right)\right)\to \left({p}{-}_{f}{a}\right)\left({b}\right)={p}\left({b}\right)-{a}\left({b}\right)$
18 8 13 15 16 17 syl22anc ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to \left({p}{-}_{f}{a}\right)\left({b}\right)={p}\left({b}\right)-{a}\left({b}\right)$
19 6 adantr ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {p}:ℂ⟶ℂ$
20 19 16 ffvelrnd ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {p}\left({b}\right)\in ℂ$
21 simprlr ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {{p}↾}_{{D}}={F}$
22 simprrr ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {{a}↾}_{{D}}={F}$
23 21 22 eqtr4d ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {{p}↾}_{{D}}={{a}↾}_{{D}}$
24 23 adantr ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {{p}↾}_{{D}}={{a}↾}_{{D}}$
25 24 fveq1d ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to \left({{p}↾}_{{D}}\right)\left({b}\right)=\left({{a}↾}_{{D}}\right)\left({b}\right)$
26 fvres ${⊢}{b}\in {D}\to \left({{p}↾}_{{D}}\right)\left({b}\right)={p}\left({b}\right)$
27 26 adantl ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to \left({{p}↾}_{{D}}\right)\left({b}\right)={p}\left({b}\right)$
28 fvres ${⊢}{b}\in {D}\to \left({{a}↾}_{{D}}\right)\left({b}\right)={a}\left({b}\right)$
29 28 adantl ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to \left({{a}↾}_{{D}}\right)\left({b}\right)={a}\left({b}\right)$
30 25 27 29 3eqtr3d ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {p}\left({b}\right)={a}\left({b}\right)$
31 20 30 subeq0bd ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to {p}\left({b}\right)-{a}\left({b}\right)=0$
32 18 31 eqtrd ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge {b}\in {D}\right)\to \left({p}{-}_{f}{a}\right)\left({b}\right)=0$
33 32 ex ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({b}\in {D}\to \left({p}{-}_{f}{a}\right)\left({b}\right)=0\right)$
34 3 33 jcad ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({b}\in {D}\to \left({b}\in ℂ\wedge \left({p}{-}_{f}{a}\right)\left({b}\right)=0\right)\right)$
35 plysubcl ${⊢}\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {a}\in \mathrm{Poly}\left(ℂ\right)\right)\to {p}{-}_{f}{a}\in \mathrm{Poly}\left(ℂ\right)$
36 4 9 35 syl2anc ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}{-}_{f}{a}\in \mathrm{Poly}\left(ℂ\right)$
37 plyf ${⊢}{p}{-}_{f}{a}\in \mathrm{Poly}\left(ℂ\right)\to \left({p}{-}_{f}{a}\right):ℂ⟶ℂ$
38 ffn ${⊢}\left({p}{-}_{f}{a}\right):ℂ⟶ℂ\to \left({p}{-}_{f}{a}\right)Fnℂ$
39 fniniseg ${⊢}\left({p}{-}_{f}{a}\right)Fnℂ\to \left({b}\in {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]↔\left({b}\in ℂ\wedge \left({p}{-}_{f}{a}\right)\left({b}\right)=0\right)\right)$
40 36 37 38 39 4syl ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({b}\in {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]↔\left({b}\in ℂ\wedge \left({p}{-}_{f}{a}\right)\left({b}\right)=0\right)\right)$
41 34 40 sylibrd ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({b}\in {D}\to {b}\in {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\right)$
42 41 ssrdv ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {D}\subseteq {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]$
43 ssfi ${⊢}\left({\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge {D}\subseteq {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\right)\to {D}\in \mathrm{Fin}$
44 43 expcom ${⊢}{D}\subseteq {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\to \left({\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\to {D}\in \mathrm{Fin}\right)$
45 42 44 syl ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\to {D}\in \mathrm{Fin}\right)$
46 1 45 mtod ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to ¬{\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}$
47 neqne ${⊢}¬{p}{-}_{f}{a}={0}_{𝑝}\to {p}{-}_{f}{a}\ne {0}_{𝑝}$
48 eqid ${⊢}{\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]={\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]$
49 48 fta1 ${⊢}\left({p}{-}_{f}{a}\in \mathrm{Poly}\left(ℂ\right)\wedge {p}{-}_{f}{a}\ne {0}_{𝑝}\right)\to \left({\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({p}{-}_{f}{a}\right)\right)$
50 36 47 49 syl2an ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge ¬{p}{-}_{f}{a}={0}_{𝑝}\right)\to \left({\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({p}{-}_{f}{a}\right)\right)$
51 50 simpld ${⊢}\left(\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\wedge ¬{p}{-}_{f}{a}={0}_{𝑝}\right)\to {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}$
52 51 ex ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left(¬{p}{-}_{f}{a}={0}_{𝑝}\to {\left({p}{-}_{f}{a}\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\right)$
53 46 52 mt3d ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}{-}_{f}{a}={0}_{𝑝}$
54 df-0p ${⊢}{0}_{𝑝}=ℂ×\left\{0\right\}$
55 53 54 syl6eq ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}{-}_{f}{a}=ℂ×\left\{0\right\}$
56 ofsubeq0 ${⊢}\left(ℂ\in \mathrm{V}\wedge {p}:ℂ⟶ℂ\wedge {a}:ℂ⟶ℂ\right)\to \left({p}{-}_{f}{a}=ℂ×\left\{0\right\}↔{p}={a}\right)$
57 14 6 11 56 mp3an2i ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to \left({p}{-}_{f}{a}=ℂ×\left\{0\right\}↔{p}={a}\right)$
58 55 57 mpbid ${⊢}\left(\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\wedge \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\right)\to {p}={a}$
59 58 ex ${⊢}\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\to \left(\left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\to {p}={a}\right)$
60 59 alrimivv ${⊢}\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\to \forall {p}\phantom{\rule{.4em}{0ex}}\forall {a}\phantom{\rule{.4em}{0ex}}\left(\left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\to {p}={a}\right)$
61 eleq1w ${⊢}{p}={a}\to \left({p}\in \mathrm{Poly}\left(ℂ\right)↔{a}\in \mathrm{Poly}\left(ℂ\right)\right)$
62 reseq1 ${⊢}{p}={a}\to {{p}↾}_{{D}}={{a}↾}_{{D}}$
63 62 eqeq1d ${⊢}{p}={a}\to \left({{p}↾}_{{D}}={F}↔{{a}↾}_{{D}}={F}\right)$
64 61 63 anbi12d ${⊢}{p}={a}\to \left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)↔\left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)$
65 64 mo4 ${⊢}{\exists }^{*}{p}\phantom{\rule{.4em}{0ex}}\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)↔\forall {p}\phantom{\rule{.4em}{0ex}}\forall {a}\phantom{\rule{.4em}{0ex}}\left(\left(\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\wedge \left({a}\in \mathrm{Poly}\left(ℂ\right)\wedge {{a}↾}_{{D}}={F}\right)\right)\to {p}={a}\right)$
66 60 65 sylibr ${⊢}\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\to {\exists }^{*}{p}\phantom{\rule{.4em}{0ex}}\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)$
67 plyssc ${⊢}\mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left(ℂ\right)$
68 67 sseli ${⊢}{p}\in \mathrm{Poly}\left({S}\right)\to {p}\in \mathrm{Poly}\left(ℂ\right)$
69 68 anim1i ${⊢}\left({p}\in \mathrm{Poly}\left({S}\right)\wedge {{p}↾}_{{D}}={F}\right)\to \left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)$
70 69 moimi ${⊢}{\exists }^{*}{p}\phantom{\rule{.4em}{0ex}}\left({p}\in \mathrm{Poly}\left(ℂ\right)\wedge {{p}↾}_{{D}}={F}\right)\to {\exists }^{*}{p}\phantom{\rule{.4em}{0ex}}\left({p}\in \mathrm{Poly}\left({S}\right)\wedge {{p}↾}_{{D}}={F}\right)$
71 66 70 syl ${⊢}\left({D}\subseteq ℂ\wedge ¬{D}\in \mathrm{Fin}\right)\to {\exists }^{*}{p}\phantom{\rule{.4em}{0ex}}\left({p}\in \mathrm{Poly}\left({S}\right)\wedge {{p}↾}_{{D}}={F}\right)$