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

Metamath Proof Explorer

Theorem coecj

Proof