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