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 C_ CC /\ -. D e. Fin ) -> E* p ( p e. ( Poly ` S ) /\ ( p |` D ) = F ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> -. D e. Fin )
2 simpll 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> D C_ CC )
3 2 sseld 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( b e. D -> b e. CC ) )
4 simprll 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> p e. ( Poly ` CC ) )
5 plyf 
 |-  ( p e. ( Poly ` CC ) -> p : CC --> CC )
6 4 5 syl 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> p : CC --> CC )
7 6 ffnd 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> p Fn CC )
8 7 adantr 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> p Fn CC )
9 simprrl 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> a e. ( Poly ` CC ) )
10 plyf 
 |-  ( a e. ( Poly ` CC ) -> a : CC --> CC )
11 9 10 syl 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> a : CC --> CC )
12 11 ffnd 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> a Fn CC )
13 12 adantr 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> a Fn CC )
14 cnex 
 |-  CC e. _V
15 14 a1i 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> CC e. _V )
16 2 sselda 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> b e. CC )
17 fnfvof 
 |-  ( ( ( p Fn CC /\ a Fn CC ) /\ ( CC e. _V /\ b e. CC ) ) -> ( ( p oF - a ) ` b ) = ( ( p ` b ) - ( a ` b ) ) )
18 8 13 15 16 17 syl22anc 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( ( p oF - a ) ` b ) = ( ( p ` b ) - ( a ` b ) ) )
19 6 adantr 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> p : CC --> CC )
20 19 16 ffvelrnd 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( p ` b ) e. CC )
21 simprlr 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( p |` D ) = F )
22 simprrr 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( a |` D ) = F )
23 21 22 eqtr4d 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( p |` D ) = ( a |` D ) )
24 23 adantr 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( p |` D ) = ( a |` D ) )
25 24 fveq1d 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( ( p |` D ) ` b ) = ( ( a |` D ) ` b ) )
26 fvres 
 |-  ( b e. D -> ( ( p |` D ) ` b ) = ( p ` b ) )
27 26 adantl 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( ( p |` D ) ` b ) = ( p ` b ) )
28 fvres 
 |-  ( b e. D -> ( ( a |` D ) ` b ) = ( a ` b ) )
29 28 adantl 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( ( a |` D ) ` b ) = ( a ` b ) )
30 25 27 29 3eqtr3d 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( p ` b ) = ( a ` b ) )
31 20 30 subeq0bd 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( ( p ` b ) - ( a ` b ) ) = 0 )
32 18 31 eqtrd 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ b e. D ) -> ( ( p oF - a ) ` b ) = 0 )
33 32 ex 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( b e. D -> ( ( p oF - a ) ` b ) = 0 ) )
34 3 33 jcad 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( b e. D -> ( b e. CC /\ ( ( p oF - a ) ` b ) = 0 ) ) )
35 plysubcl 
 |-  ( ( p e. ( Poly ` CC ) /\ a e. ( Poly ` CC ) ) -> ( p oF - a ) e. ( Poly ` CC ) )
36 4 9 35 syl2anc 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( p oF - a ) e. ( Poly ` CC ) )
37 plyf 
 |-  ( ( p oF - a ) e. ( Poly ` CC ) -> ( p oF - a ) : CC --> CC )
38 ffn 
 |-  ( ( p oF - a ) : CC --> CC -> ( p oF - a ) Fn CC )
39 fniniseg 
 |-  ( ( p oF - a ) Fn CC -> ( b e. ( `' ( p oF - a ) " { 0 } ) <-> ( b e. CC /\ ( ( p oF - a ) ` b ) = 0 ) ) )
40 36 37 38 39 4syl 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( b e. ( `' ( p oF - a ) " { 0 } ) <-> ( b e. CC /\ ( ( p oF - a ) ` b ) = 0 ) ) )
41 34 40 sylibrd 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( b e. D -> b e. ( `' ( p oF - a ) " { 0 } ) ) )
42 41 ssrdv 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> D C_ ( `' ( p oF - a ) " { 0 } ) )
43 ssfi 
 |-  ( ( ( `' ( p oF - a ) " { 0 } ) e. Fin /\ D C_ ( `' ( p oF - a ) " { 0 } ) ) -> D e. Fin )
44 43 expcom 
 |-  ( D C_ ( `' ( p oF - a ) " { 0 } ) -> ( ( `' ( p oF - a ) " { 0 } ) e. Fin -> D e. Fin ) )
45 42 44 syl 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( ( `' ( p oF - a ) " { 0 } ) e. Fin -> D e. Fin ) )
46 1 45 mtod 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> -. ( `' ( p oF - a ) " { 0 } ) e. Fin )
47 neqne 
 |-  ( -. ( p oF - a ) = 0p -> ( p oF - a ) =/= 0p )
48 eqid 
 |-  ( `' ( p oF - a ) " { 0 } ) = ( `' ( p oF - a ) " { 0 } )
49 48 fta1 
 |-  ( ( ( p oF - a ) e. ( Poly ` CC ) /\ ( p oF - a ) =/= 0p ) -> ( ( `' ( p oF - a ) " { 0 } ) e. Fin /\ ( # ` ( `' ( p oF - a ) " { 0 } ) ) <_ ( deg ` ( p oF - a ) ) ) )
50 36 47 49 syl2an 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ -. ( p oF - a ) = 0p ) -> ( ( `' ( p oF - a ) " { 0 } ) e. Fin /\ ( # ` ( `' ( p oF - a ) " { 0 } ) ) <_ ( deg ` ( p oF - a ) ) ) )
51 50 simpld 
 |-  ( ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) /\ -. ( p oF - a ) = 0p ) -> ( `' ( p oF - a ) " { 0 } ) e. Fin )
52 51 ex 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( -. ( p oF - a ) = 0p -> ( `' ( p oF - a ) " { 0 } ) e. Fin ) )
53 46 52 mt3d 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( p oF - a ) = 0p )
54 df-0p 
 |-  0p = ( CC X. { 0 } )
55 53 54 eqtrdi 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( p oF - a ) = ( CC X. { 0 } ) )
56 ofsubeq0 
 |-  ( ( CC e. _V /\ p : CC --> CC /\ a : CC --> CC ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
57 14 6 11 56 mp3an2i 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
58 55 57 mpbid 
 |-  ( ( ( D C_ CC /\ -. D e. Fin ) /\ ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) ) -> p = a )
59 58 ex 
 |-  ( ( D C_ CC /\ -. D e. Fin ) -> ( ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) -> p = a ) )
60 59 alrimivv 
 |-  ( ( D C_ CC /\ -. D e. Fin ) -> A. p A. a ( ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) -> p = a ) )
61 eleq1w 
 |-  ( p = a -> ( p e. ( Poly ` CC ) <-> a e. ( Poly ` CC ) ) )
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 e. ( Poly ` CC ) /\ ( p |` D ) = F ) <-> ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) )
65 64 mo4 
 |-  ( E* p ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) <-> A. p A. a ( ( ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) /\ ( a e. ( Poly ` CC ) /\ ( a |` D ) = F ) ) -> p = a ) )
66 60 65 sylibr 
 |-  ( ( D C_ CC /\ -. D e. Fin ) -> E* p ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) )
67 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
68 67 sseli 
 |-  ( p e. ( Poly ` S ) -> p e. ( Poly ` CC ) )
69 68 anim1i 
 |-  ( ( p e. ( Poly ` S ) /\ ( p |` D ) = F ) -> ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) )
70 69 moimi 
 |-  ( E* p ( p e. ( Poly ` CC ) /\ ( p |` D ) = F ) -> E* p ( p e. ( Poly ` S ) /\ ( p |` D ) = F ) )
71 66 70 syl 
 |-  ( ( D C_ CC /\ -. D e. Fin ) -> E* p ( p e. ( Poly ` S ) /\ ( p |` D ) = F ) )