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 ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐹 ‘ ( ∗ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( 0 ... ( deg ‘ 𝐹 ) ) ∈ Fin )
2 0re ⊢ 0 ∈ ℝ
3 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
4 3 coef2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 0 ∈ ℝ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
5 2 4 mpan2 ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
7 elfznn0 ⊢ ( 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑥 ∈ ℕ0 )
8 ffvelcdm ⊢ ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ ∧ 𝑥 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
9 6 7 8 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
10 9 recnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
11 simpr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ℂ )
12 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑥 ) ∈ ℂ )
13 11 7 12 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝐴 ↑ 𝑥 ) ∈ ℂ )
14 10 13 mulcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ∈ ℂ )
15 1 14 fsumcj ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) = Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ∗ ‘ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) )
16 10 13 cjmuld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ∗ ‘ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) = ( ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) ) · ( ∗ ‘ ( 𝐴 ↑ 𝑥 ) ) ) )
17 9 cjred ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) ) = ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) )
18 cjexp ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0 ) → ( ∗ ‘ ( 𝐴 ↑ 𝑥 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) )
19 11 7 18 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ∗ ‘ ( 𝐴 ↑ 𝑥 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) )
20 17 19 oveq12d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) ) · ( ∗ ‘ ( 𝐴 ↑ 𝑥 ) ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) ) )
21 16 20 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ∗ ‘ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) ) )
22 21 sumeq2dv ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ∗ ‘ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) = Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) ) )
23 15 22 eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) = Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) ) )
24 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
25 3 24 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ‘ 𝐴 ) = Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) )
26 25 fveq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( 𝐹 ‘ 𝐴 ) ) = ( ∗ ‘ Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( 𝐴 ↑ 𝑥 ) ) ) )
27 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
28 3 24 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( 𝐹 ‘ ( ∗ ‘ 𝐴 ) ) = Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) ) )
29 27 28 sylan2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ‘ ( ∗ ‘ 𝐴 ) ) = Σ 𝑥 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑥 ) · ( ( ∗ ‘ 𝐴 ) ↑ 𝑥 ) ) )
30 23 26 29 3eqtr4d ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐹 ‘ ( ∗ ‘ 𝐴 ) ) )