Metamath Proof Explorer

Theorem ply1term

Description: A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypothesis ply1term.1 
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
Assertion ply1term 
|- ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> F e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 ply1term.1 
 |-  F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
2 ssel2 
 |-  ( ( S C_ CC /\ A e. S ) -> A e. CC )
3 1 ply1termlem 
 |-  ( ( A e. CC /\ N e. NN0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) )
4 2 3 stoic3 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) )
5 simp1 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> S C_ CC )
6 0cnd 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> 0 e. CC )
7 6 snssd 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> { 0 } C_ CC )
8 5 7 unssd 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> ( S u. { 0 } ) C_ CC )
9 simp3 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> N e. NN0 )
10 simpl2 
 |-  ( ( ( S C_ CC /\ A e. S /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> A e. S )
11 elun1 
 |-  ( A e. S -> A e. ( S u. { 0 } ) )
12 10 11 syl 
 |-  ( ( ( S C_ CC /\ A e. S /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> A e. ( S u. { 0 } ) )
13 ssun2 
 |-  { 0 } C_ ( S u. { 0 } )
14 c0ex 
 |-  0 e. _V
15 14 snss 
 |-  ( 0 e. ( S u. { 0 } ) <-> { 0 } C_ ( S u. { 0 } ) )
16 13 15 mpbir 
 |-  0 e. ( S u. { 0 } )
17 ifcl 
 |-  ( ( A e. ( S u. { 0 } ) /\ 0 e. ( S u. { 0 } ) ) -> if ( k = N , A , 0 ) e. ( S u. { 0 } ) )
18 12 16 17 sylancl 
 |-  ( ( ( S C_ CC /\ A e. S /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> if ( k = N , A , 0 ) e. ( S u. { 0 } ) )
19 8 9 18 elplyd 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) e. ( Poly ` ( S u. { 0 } ) ) )
20 4 19 eqeltrd 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> F e. ( Poly ` ( S u. { 0 } ) ) )
21 plyun0 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )
22 20 21 eleqtrdi 
 |-  ( ( S C_ CC /\ A e. S /\ N e. NN0 ) -> F e. ( Poly ` S ) )