Metamath Proof Explorer

Theorem coecj

Description: Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycj.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
plycj.2 ⊢ 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
coecj.3 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion coecj ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐺 ) = ( ∗ ∘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 plycj.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 plycj.2 ⊢ 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
3 coecj.3 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
4 cjcl ⊢ ( 𝑥 ∈ ℂ → ( ∗ ‘ 𝑥 ) ∈ ℂ )
5 4 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( ∗ ‘ 𝑥 ) ∈ ℂ )
6 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
7 6 sseli ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
8 1 2 5 7 plycj ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
9 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
10 1 9 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
11 cjf ⊢ ∗ : ℂ ⟶ ℂ
12 3 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
13 fco ⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ∗ ∘ 𝐴 ) : ℕ0 ⟶ ℂ )
14 11 12 13 sylancr ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∗ ∘ 𝐴 ) : ℕ0 ⟶ ℂ )
15 fvco3 ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) = ( ∗ ‘ ( 𝐴 ‘ 𝑘 ) ) )
16 12 15 sylan ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) = ( ∗ ‘ ( 𝐴 ‘ 𝑘 ) ) )
17 cj0 ⊢ ( ∗ ‘ 0 ) = 0
18 17 eqcomi ⊢ 0 = ( ∗ ‘ 0 )
19 18 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → 0 = ( ∗ ‘ 0 ) )
20 16 19 eqeq12d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) = 0 ↔ ( ∗ ‘ ( 𝐴 ‘ 𝑘 ) ) = ( ∗ ‘ 0 ) ) )
21 12 ffvelrnda ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
22 0cnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → 0 ∈ ℂ )
23 cj11 ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 ‘ 𝑘 ) ) = ( ∗ ‘ 0 ) ↔ ( 𝐴 ‘ 𝑘 ) = 0 ) )
24 21 22 23 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ‘ ( 𝐴 ‘ 𝑘 ) ) = ( ∗ ‘ 0 ) ↔ ( 𝐴 ‘ 𝑘 ) = 0 ) )
25 20 24 bitrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) = 0 ↔ ( 𝐴 ‘ 𝑘 ) = 0 ) )
26 25 necon3bid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) ≠ 0 ↔ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) )
27 3 1 dgrub2 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
28 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
29 10 12 28 syl2anc ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
30 27 29 mpbid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
31 30 r19.21bi ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
32 26 31 sylbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
33 32 ralrimiva ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑘 ∈ ℕ0 ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
34 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ∗ ∘ 𝐴 ) : ℕ0 ⟶ ℂ ) → ( ( ( ∗ ∘ 𝐴 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
35 10 14 34 syl2anc ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( ( ∗ ∘ 𝐴 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
36 33 35 mpbird ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( ∗ ∘ 𝐴 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
37 1 2 3 plycjlem ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
38 8 10 14 36 37 coeeq ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐺 ) = ( ∗ ∘ 𝐴 ) )