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	$⊢ N = \deg (F)$
	plycj.2	$⊢ G = (* \circ F) \circ *$
	coecj.3	$⊢ A = coeff (F)$
Assertion	coecj	$⊢ F \in Poly (S) \to coeff (G) = * \circ A$

Proof

Step	Hyp	Ref	Expression
1		plycj.1	$⊢ N = \deg (F)$
2		plycj.2	$⊢ G = (* \circ F) \circ *$
3		coecj.3	$⊢ A = coeff (F)$
4		cjcl	$⊢ x \in ℂ \to \overline{x} \in ℂ$
5	4	adantl	$⊢ (F \in Poly (S) \land x \in ℂ) \to \overline{x} \in ℂ$
6		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
7	6	sseli	$⊢ F \in Poly (S) \to F \in Poly (ℂ)$
8	1 2 5 7	plycj	$⊢ F \in Poly (S) \to G \in Poly (ℂ)$
9		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
10	1 9	eqeltrid	$⊢ F \in Poly (S) \to N \in ℕ_{0}$
11		cjf	$⊢ * : ℂ ⟶ ℂ$
12	3	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
13		fco	$⊢ (* : ℂ ⟶ ℂ \land A : ℕ_{0} ⟶ ℂ) \to (* \circ A) : ℕ_{0} ⟶ ℂ$
14	11 12 13	sylancr	$⊢ F \in Poly (S) \to (* \circ A) : ℕ_{0} ⟶ ℂ$
15		fvco3	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to (* \circ A) (k) = \overline{A (k)}$
16	12 15	sylan	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (* \circ A) (k) = \overline{A (k)}$
17		cj0	$⊢ \overline{0} = 0$
18	17	eqcomi	$⊢ 0 = \overline{0}$
19	18	a1i	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to 0 = \overline{0}$
20	16 19	eqeq12d	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to ((* \circ A) (k) = 0 \leftrightarrow \overline{A (k)} = \overline{0})$
21	12	ffvelrnda	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to A (k) \in ℂ$
22		0cnd	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to 0 \in ℂ$
23		cj11	$⊢ (A (k) \in ℂ \land 0 \in ℂ) \to (\overline{A (k)} = \overline{0} \leftrightarrow A (k) = 0)$
24	21 22 23	syl2anc	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (\overline{A (k)} = \overline{0} \leftrightarrow A (k) = 0)$
25	20 24	bitrd	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to ((* \circ A) (k) = 0 \leftrightarrow A (k) = 0)$
26	25	necon3bid	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to ((* \circ A) (k) \neq 0 \leftrightarrow A (k) \neq 0)$
27	3 1	dgrub2	$⊢ F \in Poly (S) \to A [ℤ_{\geq (N + 1)}] = \{0\}$
28		plyco0	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N))$
29	10 12 28	syl2anc	$⊢ F \in Poly (S) \to (A [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N))$
30	27 29	mpbid	$⊢ F \in Poly (S) \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)$
31	30	r19.21bi	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq N)$
32	26 31	sylbid	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to ((* \circ A) (k) \neq 0 \to k \leq N)$
33	32	ralrimiva	$⊢ F \in Poly (S) \to \forall k \in ℕ_{0} ((* \circ A) (k) \neq 0 \to k \leq N)$
34		plyco0	$⊢ (N \in ℕ_{0} \land (* \circ A) : ℕ_{0} ⟶ ℂ) \to ((* \circ A) [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((* \circ A) (k) \neq 0 \to k \leq N))$
35	10 14 34	syl2anc	$⊢ F \in Poly (S) \to ((* \circ A) [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((* \circ A) (k) \neq 0 \to k \leq N))$
36	33 35	mpbird	$⊢ F \in Poly (S) \to (* \circ A) [ℤ_{\geq (N + 1)}] = \{0\}$
37	1 2 3	plycjlem	$⊢ F \in Poly (S) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} (* \circ A) (k) z^{k})$
38	8 10 14 36 37	coeeq	$⊢ F \in Poly (S) \to coeff (G) = * \circ A$

Metamath Proof Explorer

Theorem coecj

Proof