This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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.2 ⊢ 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
coecj.3 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion coecj ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐺 ) = ( ∗ ∘ 𝐴 ) )

Proof

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