# 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 )`
` |-  ( ( 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 ) )`