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 D ¬ D Fin * p p Poly S p D = F

Proof

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