Metamath Proof Explorer

Theorem elplyr

Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion elplyr 
|- ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> S C_ CC )
2 simp2 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> N e. NN0 )
3 simp3 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> A : NN0 --> S )
4 ssun1 
 |-  S C_ ( S u. { 0 } )
5 fss 
 |-  ( ( A : NN0 --> S /\ S C_ ( S u. { 0 } ) ) -> A : NN0 --> ( S u. { 0 } ) )
6 3 4 5 sylancl 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> A : NN0 --> ( S u. { 0 } ) )
7 0cnd 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> 0 e. CC )
8 7 snssd 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> { 0 } C_ CC )
9 1 8 unssd 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( S u. { 0 } ) C_ CC )
10 cnex 
 |-  CC e. _V
11 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
12 9 10 11 sylancl 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( S u. { 0 } ) e. _V )
13 nn0ex 
 |-  NN0 e. _V
14 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
15 12 13 14 sylancl 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
16 6 15 mpbird 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
17 eqidd 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
18 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
19 18 sumeq1d 
 |-  ( n = N -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( a ` k ) x. ( z ^ k ) ) )
20 19 mpteq2dv 
 |-  ( n = N -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( a ` k ) x. ( z ^ k ) ) ) )
21 20 eqeq2d 
 |-  ( n = N -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
22 fveq1 
 |-  ( a = A -> ( a ` k ) = ( A ` k ) )
23 22 oveq1d 
 |-  ( a = A -> ( ( a ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( z ^ k ) ) )
24 23 sumeq2sdv 
 |-  ( a = A -> sum_ k e. ( 0 ... N ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) )
25 24 mpteq2dv 
 |-  ( a = A -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
26 25 eqeq2d 
 |-  ( a = A -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
27 21 26 rspc2ev 
 |-  ( ( N e. NN0 /\ A e. ( ( S u. { 0 } ) ^m NN0 ) /\ ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
28 2 16 17 27 syl3anc 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
29 elply 
 |-  ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
30 1 28 29 sylanbrc 
 |-  ( ( S C_ CC /\ N e. NN0 /\ A : NN0 --> S ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) e. ( Poly ` S ) )