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 ‘ 𝑆 ) ∧ ( 𝑝𝐷 ) = 𝐹 ) )