Metamath Proof Explorer

Theorem plyrecj

Description: A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion plyrecj 
|- ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( * ` ( F ` A ) ) = ( F ` ( * ` A ) ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( 0 ... ( deg ` F ) ) e. Fin )
2 0re 
 |-  0 e. RR
3 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
4 3 coef2 
 |-  ( ( F e. ( Poly ` RR ) /\ 0 e. RR ) -> ( coeff ` F ) : NN0 --> RR )
5 2 4 mpan2 
 |-  ( F e. ( Poly ` RR ) -> ( coeff ` F ) : NN0 --> RR )
6 5 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( coeff ` F ) : NN0 --> RR )
7 elfznn0 
 |-  ( x e. ( 0 ... ( deg ` F ) ) -> x e. NN0 )
8 ffvelrn 
 |-  ( ( ( coeff ` F ) : NN0 --> RR /\ x e. NN0 ) -> ( ( coeff ` F ) ` x ) e. RR )
9 6 7 8 syl2an 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( ( coeff ` F ) ` x ) e. RR )
10 9 recnd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( ( coeff ` F ) ` x ) e. CC )
11 simpr 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> A e. CC )
12 expcl 
 |-  ( ( A e. CC /\ x e. NN0 ) -> ( A ^ x ) e. CC )
13 11 7 12 syl2an 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( A ^ x ) e. CC )
14 10 13 mulcld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) e. CC )
15 1 14 fsumcj 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( * ` sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) = sum_ x e. ( 0 ... ( deg ` F ) ) ( * ` ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) )
16 10 13 cjmuld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( * ` ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) = ( ( * ` ( ( coeff ` F ) ` x ) ) x. ( * ` ( A ^ x ) ) ) )
17 9 cjred 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( * ` ( ( coeff ` F ) ` x ) ) = ( ( coeff ` F ) ` x ) )
18 cjexp 
 |-  ( ( A e. CC /\ x e. NN0 ) -> ( * ` ( A ^ x ) ) = ( ( * ` A ) ^ x ) )
19 11 7 18 syl2an 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( * ` ( A ^ x ) ) = ( ( * ` A ) ^ x ) )
20 17 19 oveq12d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( ( * ` ( ( coeff ` F ) ` x ) ) x. ( * ` ( A ^ x ) ) ) = ( ( ( coeff ` F ) ` x ) x. ( ( * ` A ) ^ x ) ) )
21 16 20 eqtrd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ A e. CC ) /\ x e. ( 0 ... ( deg ` F ) ) ) -> ( * ` ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) = ( ( ( coeff ` F ) ` x ) x. ( ( * ` A ) ^ x ) ) )
22 21 sumeq2dv 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> sum_ x e. ( 0 ... ( deg ` F ) ) ( * ` ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) = sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( ( * ` A ) ^ x ) ) )
23 15 22 eqtrd 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( * ` sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) = sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( ( * ` A ) ^ x ) ) )
24 eqid 
 |-  ( deg ` F ) = ( deg ` F )
25 3 24 coeid2 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( F ` A ) = sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) )
26 25 fveq2d 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( * ` ( F ` A ) ) = ( * ` sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( A ^ x ) ) ) )
27 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
28 3 24 coeid2 
 |-  ( ( F e. ( Poly ` RR ) /\ ( * ` A ) e. CC ) -> ( F ` ( * ` A ) ) = sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( ( * ` A ) ^ x ) ) )
29 27 28 sylan2 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( F ` ( * ` A ) ) = sum_ x e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` x ) x. ( ( * ` A ) ^ x ) ) )
30 23 26 29 3eqtr4d 
 |-  ( ( F e. ( Poly ` RR ) /\ A e. CC ) -> ( * ` ( F ` A ) ) = ( F ` ( * ` A ) ) )