# Metamath Proof Explorer

## Theorem plycj

Description: The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on ( *z ) independently of z .) (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycj.1
`|- N = ( deg ` F )`
plycj.2
`|- G = ( ( * o. F ) o. * )`
plycj.3
`|- ( ( ph /\ x e. S ) -> ( * ` x ) e. S )`
plycj.4
`|- ( ph -> F e. ( Poly ` S ) )`
Assertion plycj
`|- ( ph -> G e. ( Poly ` S ) )`

### Proof

Step Hyp Ref Expression
1 plycj.1
` |-  N = ( deg ` F )`
2 plycj.2
` |-  G = ( ( * o. F ) o. * )`
3 plycj.3
` |-  ( ( ph /\ x e. S ) -> ( * ` x ) e. S )`
4 plycj.4
` |-  ( ph -> F e. ( Poly ` S ) )`
5 eqid
` |-  ( coeff ` F ) = ( coeff ` F )`
6 1 2 5 plycjlem
` |-  ( F e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) )`
7 4 6 syl
` |-  ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) )`
8 plybss
` |-  ( F e. ( Poly ` S ) -> S C_ CC )`
9 4 8 syl
` |-  ( ph -> S C_ CC )`
10 0cnd
` |-  ( ph -> 0 e. CC )`
11 10 snssd
` |-  ( ph -> { 0 } C_ CC )`
12 9 11 unssd
` |-  ( ph -> ( S u. { 0 } ) C_ CC )`
13 dgrcl
` |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )`
14 4 13 syl
` |-  ( ph -> ( deg ` F ) e. NN0 )`
15 1 14 eqeltrid
` |-  ( ph -> N e. NN0 )`
16 5 coef
` |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> ( S u. { 0 } ) )`
17 4 16 syl
` |-  ( ph -> ( coeff ` F ) : NN0 --> ( S u. { 0 } ) )`
18 elfznn0
` |-  ( k e. ( 0 ... N ) -> k e. NN0 )`
19 fvco3
` |-  ( ( ( coeff ` F ) : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( ( * o. ( coeff ` F ) ) ` k ) = ( * ` ( ( coeff ` F ) ` k ) ) )`
20 17 18 19 syl2an
` |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( * o. ( coeff ` F ) ) ` k ) = ( * ` ( ( coeff ` F ) ` k ) ) )`
21 ffvelrn
` |-  ( ( ( coeff ` F ) : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) )`
22 17 18 21 syl2an
` |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) )`
23 3 ralrimiva
` |-  ( ph -> A. x e. S ( * ` x ) e. S )`
24 fveq2
` |-  ( x = ( ( coeff ` F ) ` k ) -> ( * ` x ) = ( * ` ( ( coeff ` F ) ` k ) ) )`
25 24 eleq1d
` |-  ( x = ( ( coeff ` F ) ` k ) -> ( ( * ` x ) e. S <-> ( * ` ( ( coeff ` F ) ` k ) ) e. S ) )`
26 25 rspccv
` |-  ( A. x e. S ( * ` x ) e. S -> ( ( ( coeff ` F ) ` k ) e. S -> ( * ` ( ( coeff ` F ) ` k ) ) e. S ) )`
27 23 26 syl
` |-  ( ph -> ( ( ( coeff ` F ) ` k ) e. S -> ( * ` ( ( coeff ` F ) ` k ) ) e. S ) )`
28 elsni
` |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( ( coeff ` F ) ` k ) = 0 )`
29 28 fveq2d
` |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) = ( * ` 0 ) )`
30 cj0
` |-  ( * ` 0 ) = 0`
31 29 30 eqtrdi
` |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) = 0 )`
32 fvex
` |-  ( * ` ( ( coeff ` F ) ` k ) ) e. _V`
33 32 elsn
` |-  ( ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } <-> ( * ` ( ( coeff ` F ) ` k ) ) = 0 )`
34 31 33 sylibr
` |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } )`
35 34 a1i
` |-  ( ph -> ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } ) )`
36 27 35 orim12d
` |-  ( ph -> ( ( ( ( coeff ` F ) ` k ) e. S \/ ( ( coeff ` F ) ` k ) e. { 0 } ) -> ( ( * ` ( ( coeff ` F ) ` k ) ) e. S \/ ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } ) ) )`
37 elun
` |-  ( ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) <-> ( ( ( coeff ` F ) ` k ) e. S \/ ( ( coeff ` F ) ` k ) e. { 0 } ) )`
38 elun
` |-  ( ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) <-> ( ( * ` ( ( coeff ` F ) ` k ) ) e. S \/ ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } ) )`
39 36 37 38 3imtr4g
` |-  ( ph -> ( ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) ) )`
` |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) ) )`
` |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) )`
` |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( * o. ( coeff ` F ) ) ` k ) e. ( S u. { 0 } ) )`
` |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) e. ( Poly ` ( S u. { 0 } ) ) )`
` |-  ( ph -> G e. ( Poly ` ( S u. { 0 } ) ) )`
` |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )`
` |-  ( ph -> G e. ( Poly ` S ) )`