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 ) )