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 ‘ 𝐺 ) = ( ∗ ∘ 𝐴 ) )