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.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.2 
 |-  G = ( ( * o. F ) o. * )
2 plycj.3 
 |-  ( ( ph /\ x e. S ) -> ( * ` x ) e. S )
3 plycj.4 
 |-  ( ph -> F e. ( Poly ` S ) )
4 eqid 
 |-  ( deg ` F ) = ( deg ` F )
5 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
6 4 1 5 plycjlem 
 |-  ( F e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) )
7 3 6 syl 
 |-  ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) )
8 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
9 3 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 3 13 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
15 5 coef 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> ( S u. { 0 } ) )
16 3 15 syl 
 |-  ( ph -> ( coeff ` F ) : NN0 --> ( S u. { 0 } ) )
17 elfznn0 
 |-  ( k e. ( 0 ... ( deg ` F ) ) -> k e. NN0 )
18 fvco3 
 |-  ( ( ( coeff ` F ) : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( ( * o. ( coeff ` F ) ) ` k ) = ( * ` ( ( coeff ` F ) ` k ) ) )
19 16 17 18 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( ( * o. ( coeff ` F ) ) ` k ) = ( * ` ( ( coeff ` F ) ` k ) ) )
20 ffvelcdm 
 |-  ( ( ( coeff ` F ) : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) )
21 16 17 20 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) )
22 2 ralrimiva 
 |-  ( ph -> A. x e. S ( * ` x ) e. S )
23 fveq2 
 |-  ( x = ( ( coeff ` F ) ` k ) -> ( * ` x ) = ( * ` ( ( coeff ` F ) ` k ) ) )
24 23 eleq1d 
 |-  ( x = ( ( coeff ` F ) ` k ) -> ( ( * ` x ) e. S <-> ( * ` ( ( coeff ` F ) ` k ) ) e. S ) )
25 24 rspccv 
 |-  ( A. x e. S ( * ` x ) e. S -> ( ( ( coeff ` F ) ` k ) e. S -> ( * ` ( ( coeff ` F ) ` k ) ) e. S ) )
26 22 25 syl 
 |-  ( ph -> ( ( ( coeff ` F ) ` k ) e. S -> ( * ` ( ( coeff ` F ) ` k ) ) e. S ) )
27 elsni 
 |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( ( coeff ` F ) ` k ) = 0 )
28 27 fveq2d 
 |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) = ( * ` 0 ) )
29 cj0 
 |-  ( * ` 0 ) = 0
30 28 29 eqtrdi 
 |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) = 0 )
31 fvex 
 |-  ( * ` ( ( coeff ` F ) ` k ) ) e. _V
32 31 elsn 
 |-  ( ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } <-> ( * ` ( ( coeff ` F ) ` k ) ) = 0 )
33 30 32 sylibr 
 |-  ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } )
34 33 a1i 
 |-  ( ph -> ( ( ( coeff ` F ) ` k ) e. { 0 } -> ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } ) )
35 26 34 orim12d 
 |-  ( ph -> ( ( ( ( coeff ` F ) ` k ) e. S \/ ( ( coeff ` F ) ` k ) e. { 0 } ) -> ( ( * ` ( ( coeff ` F ) ` k ) ) e. S \/ ( * ` ( ( coeff ` F ) ` k ) ) e. { 0 } ) ) )
36 elun 
 |-  ( ( ( coeff ` F ) ` k ) e. ( S u. { 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 35 36 37 3imtr4g 
 |-  ( ph -> ( ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) ) )
39 38 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( coeff ` F ) ` k ) e. ( S u. { 0 } ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) ) )
40 21 39 mpd 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( * ` ( ( coeff ` F ) ` k ) ) e. ( S u. { 0 } ) )
41 19 40 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( ( * o. ( coeff ` F ) ) ` k ) e. ( S u. { 0 } ) )
42 12 14 41 elplyd 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( * o. ( coeff ` F ) ) ` k ) x. ( z ^ k ) ) ) e. ( Poly ` ( S u. { 0 } ) ) )
43 7 42 eqeltrd 
 |-  ( ph -> G e. ( Poly ` ( S u. { 0 } ) ) )
44 plyun0 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )
45 43 44 eleqtrdi 
 |-  ( ph -> G e. ( Poly ` S ) )