Metamath Proof Explorer

Theorem coecj

Description: Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycj.1 
|- N = ( deg ` F )
plycj.2 
|- G = ( ( * o. F ) o. * )
coecj.3 
|- A = ( coeff ` F )
Assertion coecj 
|- ( F e. ( Poly ` S ) -> ( coeff ` G ) = ( * o. A ) )

Proof

Step Hyp Ref Expression
1 plycj.1 
 |-  N = ( deg ` F )
2 plycj.2 
 |-  G = ( ( * o. F ) o. * )
3 coecj.3 
 |-  A = ( coeff ` F )
4 cjcl 
 |-  ( x e. CC -> ( * ` x ) e. CC )
5 4 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( * ` x ) e. CC )
6 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
7 6 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
8 1 2 5 7 plycj 
 |-  ( F e. ( Poly ` S ) -> G e. ( Poly ` CC ) )
9 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
10 1 9 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
11 cjf 
 |-  * : CC --> CC
12 3 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
13 fco 
 |-  ( ( * : CC --> CC /\ A : NN0 --> CC ) -> ( * o. A ) : NN0 --> CC )
14 11 12 13 sylancr 
 |-  ( F e. ( Poly ` S ) -> ( * o. A ) : NN0 --> CC )
15 fvco3 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( ( * o. A ) ` k ) = ( * ` ( A ` k ) ) )
16 12 15 sylan 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( * o. A ) ` k ) = ( * ` ( A ` k ) ) )
17 cj0 
 |-  ( * ` 0 ) = 0
18 17 eqcomi 
 |-  0 = ( * ` 0 )
19 18 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> 0 = ( * ` 0 ) )
20 16 19 eqeq12d 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) = 0 <-> ( * ` ( A ` k ) ) = ( * ` 0 ) ) )
21 12 ffvelrnda 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
22 0cnd 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> 0 e. CC )
23 cj11 
 |-  ( ( ( A ` k ) e. CC /\ 0 e. CC ) -> ( ( * ` ( A ` k ) ) = ( * ` 0 ) <-> ( A ` k ) = 0 ) )
24 21 22 23 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( * ` ( A ` k ) ) = ( * ` 0 ) <-> ( A ` k ) = 0 ) )
25 20 24 bitrd 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) = 0 <-> ( A ` k ) = 0 ) )
26 25 necon3bid 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) =/= 0 <-> ( A ` k ) =/= 0 ) )
27 3 1 dgrub2 
 |-  ( F e. ( Poly ` S ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
28 plyco0 
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
29 10 12 28 syl2anc 
 |-  ( F e. ( Poly ` S ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
30 27 29 mpbid 
 |-  ( F e. ( Poly ` S ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
31 30 r19.21bi 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
32 26 31 sylbid 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) =/= 0 -> k <_ N ) )
33 32 ralrimiva 
 |-  ( F e. ( Poly ` S ) -> A. k e. NN0 ( ( ( * o. A ) ` k ) =/= 0 -> k <_ N ) )
34 plyco0 
 |-  ( ( N e. NN0 /\ ( * o. A ) : NN0 --> CC ) -> ( ( ( * o. A ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( * o. A ) ` k ) =/= 0 -> k <_ N ) ) )
35 10 14 34 syl2anc 
 |-  ( F e. ( Poly ` S ) -> ( ( ( * o. A ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( * o. A ) ` k ) =/= 0 -> k <_ N ) ) )
36 33 35 mpbird 
 |-  ( F e. ( Poly ` S ) -> ( ( * o. A ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
37 1 2 3 plycjlem 
 |-  ( F e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
38 8 10 14 36 37 coeeq 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` G ) = ( * o. A ) )