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 } ) ) )
40 39 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) ) )
41 22 40 mpd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) )
42 20 41 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( * o. ( coeff ` F ) ) ` k ) e. ( S u. { 0 } ) )
43 12 15 42 elplyd 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) e. ( Poly ` ( S u. { 0 } ) ) )
44 7 43 eqeltrd 
 |-  ( ph -> G e. ( Poly ` ( S u. { 0 } ) ) )
45 plyun0 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )
46 44 45 eleqtrdi 
 |-  ( ph -> G e. ( Poly ` S ) )