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 ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) → ∃* 𝑝 ( 𝑝 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ¬ 𝐷 ∈ Fin )
2 simpll ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝐷 ⊆ ℂ )
3 2 sseld ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑏 ∈ 𝐷 → 𝑏 ∈ ℂ ) )
4 simprll ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑝 ∈ ( Poly ‘ ℂ ) )
5 plyf ⊢ ( 𝑝 ∈ ( Poly ‘ ℂ ) → 𝑝 : ℂ ⟶ ℂ )
6 4 5 syl ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑝 : ℂ ⟶ ℂ )
7 6 ffnd ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑝 Fn ℂ )
8 7 adantr ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → 𝑝 Fn ℂ )
9 simprrl ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑎 ∈ ( Poly ‘ ℂ ) )
10 plyf ⊢ ( 𝑎 ∈ ( Poly ‘ ℂ ) → 𝑎 : ℂ ⟶ ℂ )
11 9 10 syl ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑎 : ℂ ⟶ ℂ )
12 11 ffnd ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑎 Fn ℂ )
13 12 adantr ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → 𝑎 Fn ℂ )
14 cnex ⊢ ℂ ∈ V
15 14 a1i ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ℂ ∈ V )
16 2 sselda ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ ℂ )
17 fnfvof ⊢ ( ( ( 𝑝 Fn ℂ ∧ 𝑎 Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑏 ∈ ℂ ) ) → ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = ( ( 𝑝 ‘ 𝑏 ) − ( 𝑎 ‘ 𝑏 ) ) )
18 8 13 15 16 17 syl22anc ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = ( ( 𝑝 ‘ 𝑏 ) − ( 𝑎 ‘ 𝑏 ) ) )
19 6 adantr ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → 𝑝 : ℂ ⟶ ℂ )
20 19 16 ffvelrnd ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( 𝑝 ‘ 𝑏 ) ∈ ℂ )
21 simprlr ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑝 ↾ 𝐷 ) = 𝐹 )
22 simprrr ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑎 ↾ 𝐷 ) = 𝐹 )
23 21 22 eqtr4d ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑝 ↾ 𝐷 ) = ( 𝑎 ↾ 𝐷 ) )
24 23 adantr ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( 𝑝 ↾ 𝐷 ) = ( 𝑎 ↾ 𝐷 ) )
25 24 fveq1d ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑝 ↾ 𝐷 ) ‘ 𝑏 ) = ( ( 𝑎 ↾ 𝐷 ) ‘ 𝑏 ) )
26 fvres ⊢ ( 𝑏 ∈ 𝐷 → ( ( 𝑝 ↾ 𝐷 ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑏 ) )
27 26 adantl ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑝 ↾ 𝐷 ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑏 ) )
28 fvres ⊢ ( 𝑏 ∈ 𝐷 → ( ( 𝑎 ↾ 𝐷 ) ‘ 𝑏 ) = ( 𝑎 ‘ 𝑏 ) )
29 28 adantl ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑎 ↾ 𝐷 ) ‘ 𝑏 ) = ( 𝑎 ‘ 𝑏 ) )
30 25 27 29 3eqtr3d ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( 𝑝 ‘ 𝑏 ) = ( 𝑎 ‘ 𝑏 ) )
31 20 30 subeq0bd ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑝 ‘ 𝑏 ) − ( 𝑎 ‘ 𝑏 ) ) = 0 )
32 18 31 eqtrd ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = 0 )
33 32 ex ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑏 ∈ 𝐷 → ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = 0 ) )
34 3 33 jcad ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑏 ∈ 𝐷 → ( 𝑏 ∈ ℂ ∧ ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = 0 ) ) )
35 plysubcl ⊢ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ 𝑎 ∈ ( Poly ‘ ℂ ) ) → ( 𝑝 ∘f − 𝑎 ) ∈ ( Poly ‘ ℂ ) )
36 4 9 35 syl2anc ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑝 ∘f − 𝑎 ) ∈ ( Poly ‘ ℂ ) )
37 plyf ⊢ ( ( 𝑝 ∘f − 𝑎 ) ∈ ( Poly ‘ ℂ ) → ( 𝑝 ∘f − 𝑎 ) : ℂ ⟶ ℂ )
38 ffn ⊢ ( ( 𝑝 ∘f − 𝑎 ) : ℂ ⟶ ℂ → ( 𝑝 ∘f − 𝑎 ) Fn ℂ )
39 fniniseg ⊢ ( ( 𝑝 ∘f − 𝑎 ) Fn ℂ → ( 𝑏 ∈ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ↔ ( 𝑏 ∈ ℂ ∧ ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = 0 ) ) )
40 36 37 38 39 4syl ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑏 ∈ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ↔ ( 𝑏 ∈ ℂ ∧ ( ( 𝑝 ∘f − 𝑎 ) ‘ 𝑏 ) = 0 ) ) )
41 34 40 sylibrd ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑏 ∈ 𝐷 → 𝑏 ∈ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ) )
42 41 ssrdv ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝐷 ⊆ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) )
43 ssfi ⊢ ( ( ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin ∧ 𝐷 ⊆ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ) → 𝐷 ∈ Fin )
44 43 expcom ⊢ ( 𝐷 ⊆ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) → ( ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin → 𝐷 ∈ Fin ) )
45 42 44 syl ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin → 𝐷 ∈ Fin ) )
46 1 45 mtod ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ¬ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin )
47 neqne ⊢ ( ¬ ( 𝑝 ∘f − 𝑎 ) = 0𝑝 → ( 𝑝 ∘f − 𝑎 ) ≠ 0𝑝 )
48 eqid ⊢ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) = ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } )
49 48 fta1 ⊢ ( ( ( 𝑝 ∘f − 𝑎 ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ∘f − 𝑎 ) ≠ 0𝑝 ) → ( ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝑝 ∘f − 𝑎 ) ) ) )
50 36 47 49 syl2an ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ ¬ ( 𝑝 ∘f − 𝑎 ) = 0𝑝 ) → ( ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝑝 ∘f − 𝑎 ) ) ) )
51 50 simpld ⊢ ( ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) ∧ ¬ ( 𝑝 ∘f − 𝑎 ) = 0𝑝 ) → ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin )
52 51 ex ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( ¬ ( 𝑝 ∘f − 𝑎 ) = 0𝑝 → ( ◡ ( 𝑝 ∘f − 𝑎 ) “ { 0 } ) ∈ Fin ) )
53 46 52 mt3d ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑝 ∘f − 𝑎 ) = 0𝑝 )
54 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
55 53 54 eqtrdi ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( 𝑝 ∘f − 𝑎 ) = ( ℂ × { 0 } ) )
56 ofsubeq0 ⊢ ( ( ℂ ∈ V ∧ 𝑝 : ℂ ⟶ ℂ ∧ 𝑎 : ℂ ⟶ ℂ ) → ( ( 𝑝 ∘f − 𝑎 ) = ( ℂ × { 0 } ) ↔ 𝑝 = 𝑎 ) )
57 14 6 11 56 mp3an2i ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → ( ( 𝑝 ∘f − 𝑎 ) = ( ℂ × { 0 } ) ↔ 𝑝 = 𝑎 ) )
58 55 57 mpbid ⊢ ( ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) ∧ ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) ) → 𝑝 = 𝑎 )
59 58 ex ⊢ ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) → ( ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) → 𝑝 = 𝑎 ) )
60 59 alrimivv ⊢ ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) → ∀ 𝑝 ∀ 𝑎 ( ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) → 𝑝 = 𝑎 ) )
61 eleq1w ⊢ ( 𝑝 = 𝑎 → ( 𝑝 ∈ ( Poly ‘ ℂ ) ↔ 𝑎 ∈ ( Poly ‘ ℂ ) ) )
62 reseq1 ⊢ ( 𝑝 = 𝑎 → ( 𝑝 ↾ 𝐷 ) = ( 𝑎 ↾ 𝐷 ) )
63 62 eqeq1d ⊢ ( 𝑝 = 𝑎 → ( ( 𝑝 ↾ 𝐷 ) = 𝐹 ↔ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) )
64 61 63 anbi12d ⊢ ( 𝑝 = 𝑎 → ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ↔ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) )
65 64 mo4 ⊢ ( ∃* 𝑝 ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ↔ ∀ 𝑝 ∀ 𝑎 ( ( ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) ∧ ( 𝑎 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑎 ↾ 𝐷 ) = 𝐹 ) ) → 𝑝 = 𝑎 ) )
66 60 65 sylibr ⊢ ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) → ∃* 𝑝 ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) )
67 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
68 67 sseli ⊢ ( 𝑝 ∈ ( Poly ‘ 𝑆 ) → 𝑝 ∈ ( Poly ‘ ℂ ) )
69 68 anim1i ⊢ ( ( 𝑝 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) → ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) )
70 69 moimi ⊢ ( ∃* 𝑝 ( 𝑝 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) → ∃* 𝑝 ( 𝑝 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) )
71 66 70 syl ⊢ ( ( 𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin ) → ∃* 𝑝 ( 𝑝 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑝 ↾ 𝐷 ) = 𝐹 ) )