Metamath Proof Explorer

Theorem coe1termlem

Description: The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis coe1term.1 
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
Assertion coe1termlem 
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( coeff ` F ) = ( n e. NN0 |-> if ( n = N , A , 0 ) ) /\ ( A =/= 0 -> ( deg ` F ) = N ) ) )

Proof

Step Hyp Ref Expression
1 coe1term.1 
 |-  F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
2 ssid 
 |-  CC C_ CC
3 1 ply1term 
 |-  ( ( CC C_ CC /\ A e. CC /\ N e. NN0 ) -> F e. ( Poly ` CC ) )
4 2 3 mp3an1 
 |-  ( ( A e. CC /\ N e. NN0 ) -> F e. ( Poly ` CC ) )
5 simpr 
 |-  ( ( A e. CC /\ N e. NN0 ) -> N e. NN0 )
6 simpl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> A e. CC )
7 0cn 
 |-  0 e. CC
8 ifcl 
 |-  ( ( A e. CC /\ 0 e. CC ) -> if ( n = N , A , 0 ) e. CC )
9 6 7 8 sylancl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> if ( n = N , A , 0 ) e. CC )
10 9 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ n e. NN0 ) -> if ( n = N , A , 0 ) e. CC )
11 10 fmpttd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( n e. NN0 |-> if ( n = N , A , 0 ) ) : NN0 --> CC )
12 eqid 
 |-  ( n e. NN0 |-> if ( n = N , A , 0 ) ) = ( n e. NN0 |-> if ( n = N , A , 0 ) )
13 eqeq1 
 |-  ( n = k -> ( n = N <-> k = N ) )
14 13 ifbid 
 |-  ( n = k -> if ( n = N , A , 0 ) = if ( k = N , A , 0 ) )
15 simpr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> k e. NN0 )
16 ifcl 
 |-  ( ( A e. CC /\ 0 e. CC ) -> if ( k = N , A , 0 ) e. CC )
17 6 7 16 sylancl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> if ( k = N , A , 0 ) e. CC )
18 17 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> if ( k = N , A , 0 ) e. CC )
19 12 14 15 18 fvmptd3 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) = if ( k = N , A , 0 ) )
20 19 neeq1d 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) =/= 0 <-> if ( k = N , A , 0 ) =/= 0 ) )
21 nn0re 
 |-  ( N e. NN0 -> N e. RR )
22 21 leidd 
 |-  ( N e. NN0 -> N <_ N )
23 22 ad2antlr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> N <_ N )
24 iffalse 
 |-  ( -. k = N -> if ( k = N , A , 0 ) = 0 )
25 24 necon1ai 
 |-  ( if ( k = N , A , 0 ) =/= 0 -> k = N )
26 25 breq1d 
 |-  ( if ( k = N , A , 0 ) =/= 0 -> ( k <_ N <-> N <_ N ) )
27 23 26 syl5ibrcom 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> ( if ( k = N , A , 0 ) =/= 0 -> k <_ N ) )
28 20 27 sylbid 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) )
29 28 ralrimiva 
 |-  ( ( A e. CC /\ N e. NN0 ) -> A. k e. NN0 ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) )
30 plyco0 
 |-  ( ( N e. NN0 /\ ( n e. NN0 |-> if ( n = N , A , 0 ) ) : NN0 --> CC ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) ) )
31 5 11 30 syl2anc 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) ) )
32 29 31 mpbird 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
33 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 ) ) ) )
34 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
35 19 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. NN0 ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = ( if ( k = N , A , 0 ) x. ( z ^ k ) ) )
36 34 35 sylan2 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = ( if ( k = N , A , 0 ) x. ( z ^ k ) ) )
37 36 sumeq2dv 
 |-  ( ( A e. CC /\ N e. NN0 ) -> sum_ k e. ( 0 ... N ) ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) )
38 37 mpteq2dv 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) )
39 33 38 eqtr4d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) x. ( z ^ k ) ) ) )
40 4 5 11 32 39 coeeq 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( coeff ` F ) = ( n e. NN0 |-> if ( n = N , A , 0 ) ) )
41 4 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> F e. ( Poly ` CC ) )
42 5 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> N e. NN0 )
43 11 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> ( n e. NN0 |-> if ( n = N , A , 0 ) ) : NN0 --> CC )
44 32 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
45 39 adantr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` k ) x. ( z ^ k ) ) ) )
46 iftrue 
 |-  ( n = N -> if ( n = N , A , 0 ) = A )
47 46 12 fvmptg 
 |-  ( ( N e. NN0 /\ A e. CC ) -> ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` N ) = A )
48 47 ancoms 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` N ) = A )
49 48 neeq1d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` N ) =/= 0 <-> A =/= 0 ) )
50 49 biimpar 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> ( ( n e. NN0 |-> if ( n = N , A , 0 ) ) ` N ) =/= 0 )
51 41 42 43 44 45 50 dgreq 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ A =/= 0 ) -> ( deg ` F ) = N )
52 51 ex 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A =/= 0 -> ( deg ` F ) = N ) )
53 40 52 jca 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( coeff ` F ) = ( n e. NN0 |-> if ( n = N , A , 0 ) ) /\ ( A =/= 0 -> ( deg ` F ) = N ) ) )