plycjlem

	Ref	Expression
Hypotheses	plycj.1	$⊢ N = \deg (F)$
	plycj.2	$⊢ G = (* \circ F) \circ *$
	plycjlem.3	$⊢ A = coeff (F)$
Assertion	plycjlem	$⊢ F \in Poly (S) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} (* \circ A) (k) z^{k})$

Proof

Step	Hyp	Ref	Expression
1		plycj.1	$⊢ N = \deg (F)$
2		plycj.2	$⊢ G = (* \circ F) \circ *$
3		plycjlem.3	$⊢ A = coeff (F)$
4		cjcl	$⊢ z \in ℂ \to \overline{z} \in ℂ$
5	4	adantl	$⊢ (F \in Poly (S) \land z \in ℂ) \to \overline{z} \in ℂ$
6		cjf	$⊢ * : ℂ ⟶ ℂ$
7	6	a1i	$⊢ F \in Poly (S) \to * : ℂ ⟶ ℂ$
8	7	feqmptd	$⊢ F \in Poly (S) \to * = (z \in ℂ ⟼ \overline{z})$
9		fzfid	$⊢ (F \in Poly (S) \land x \in ℂ) \to (0 \dots N) \in Fin$
10	3	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
11	10	adantr	$⊢ (F \in Poly (S) \land x \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
12		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
13		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
14	11 12 13	syl2an	$⊢ ((F \in Poly (S) \land x \in ℂ) \land k \in (0 \dots N)) \to A (k) \in ℂ$
15		expcl	$⊢ (x \in ℂ \land k \in ℕ_{0}) \to x^{k} \in ℂ$
16	12 15	sylan2	$⊢ (x \in ℂ \land k \in (0 \dots N)) \to x^{k} \in ℂ$
17	16	adantll	$⊢ ((F \in Poly (S) \land x \in ℂ) \land k \in (0 \dots N)) \to x^{k} \in ℂ$
18	14 17	mulcld	$⊢ ((F \in Poly (S) \land x \in ℂ) \land k \in (0 \dots N)) \to A (k) x^{k} \in ℂ$
19	9 18	fsumcl	$⊢ (F \in Poly (S) \land x \in ℂ) \to \sum_{k = 0}^{N} A (k) x^{k} \in ℂ$
20	3 1	coeid	$⊢ F \in Poly (S) \to F = (x \in ℂ ⟼ \sum_{k = 0}^{N} A (k) x^{k})$
21		fveq2	$⊢ z = \sum_{k = 0}^{N} A (k) x^{k} \to \overline{z} = \overline{\sum_{k = 0}^{N} A (k) x^{k}}$
22	19 20 8 21	fmptco	$⊢ F \in Poly (S) \to * \circ F = (x \in ℂ ⟼ \overline{\sum_{k = 0}^{N} A (k) x^{k}})$
23		oveq1	$⊢ x = \overline{z} \to x^{k} = {\overline{z}}^{k}$
24	23	oveq2d	$⊢ x = \overline{z} \to A (k) x^{k} = A (k) {\overline{z}}^{k}$
25	24	sumeq2sdv	$⊢ x = \overline{z} \to \sum_{k = 0}^{N} A (k) x^{k} = \sum_{k = 0}^{N} A (k) {\overline{z}}^{k}$
26	25	fveq2d	$⊢ x = \overline{z} \to \overline{\sum_{k = 0}^{N} A (k) x^{k}} = \overline{\sum_{k = 0}^{N} A (k) {\overline{z}}^{k}}$
27	5 8 22 26	fmptco	$⊢ F \in Poly (S) \to (* \circ F) \circ * = (z \in ℂ ⟼ \overline{\sum_{k = 0}^{N} A (k) {\overline{z}}^{k}})$
28	2 27	eqtrid	$⊢ F \in Poly (S) \to G = (z \in ℂ ⟼ \overline{\sum_{k = 0}^{N} A (k) {\overline{z}}^{k}})$
29		fzfid	$⊢ (F \in Poly (S) \land z \in ℂ) \to (0 \dots N) \in Fin$
30	10	adantr	$⊢ (F \in Poly (S) \land z \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
31	30 12 13	syl2an	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to A (k) \in ℂ$
32		expcl	$⊢ (\overline{z} \in ℂ \land k \in ℕ_{0}) \to {\overline{z}}^{k} \in ℂ$
33	5 12 32	syl2an	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to {\overline{z}}^{k} \in ℂ$
34	31 33	mulcld	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to A (k) {\overline{z}}^{k} \in ℂ$
35	29 34	fsumcj	$⊢ (F \in Poly (S) \land z \in ℂ) \to \overline{\sum_{k = 0}^{N} A (k) {\overline{z}}^{k}} = \sum_{k = 0}^{N} \overline{A (k) {\overline{z}}^{k}}$
36	31 33	cjmuld	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to \overline{A (k) {\overline{z}}^{k}} = \overline{A (k)} \overline{{\overline{z}}^{k}}$
37		fvco3	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to (* \circ A) (k) = \overline{A (k)}$
38	30 12 37	syl2an	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to (* \circ A) (k) = \overline{A (k)}$
39		cjexp	$⊢ (\overline{z} \in ℂ \land k \in ℕ_{0}) \to \overline{{\overline{z}}^{k}} = {\overline{\overline{z}}}^{k}$
40	5 12 39	syl2an	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to \overline{{\overline{z}}^{k}} = {\overline{\overline{z}}}^{k}$
41		cjcj	$⊢ z \in ℂ \to \overline{\overline{z}} = z$
42	41	ad2antlr	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to \overline{\overline{z}} = z$
43	42	oveq1d	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to {\overline{\overline{z}}}^{k} = z^{k}$
44	40 43	eqtr2d	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to z^{k} = \overline{{\overline{z}}^{k}}$
45	38 44	oveq12d	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to (* \circ A) (k) z^{k} = \overline{A (k)} \overline{{\overline{z}}^{k}}$
46	36 45	eqtr4d	$⊢ ((F \in Poly (S) \land z \in ℂ) \land k \in (0 \dots N)) \to \overline{A (k) {\overline{z}}^{k}} = (* \circ A) (k) z^{k}$
47	46	sumeq2dv	$⊢ (F \in Poly (S) \land z \in ℂ) \to \sum_{k = 0}^{N} \overline{A (k) {\overline{z}}^{k}} = \sum_{k = 0}^{N} (* \circ A) (k) z^{k}$
48	35 47	eqtrd	$⊢ (F \in Poly (S) \land z \in ℂ) \to \overline{\sum_{k = 0}^{N} A (k) {\overline{z}}^{k}} = \sum_{k = 0}^{N} (* \circ A) (k) z^{k}$
49	48	mpteq2dva	$⊢ F \in Poly (S) \to (z \in ℂ ⟼ \overline{\sum_{k = 0}^{N} A (k) {\overline{z}}^{k}}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} (* \circ A) (k) z^{k})$
50	28 49	eqtrd	$⊢ F \in Poly (S) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} (* \circ A) (k) z^{k})$

Metamath Proof Explorer

Theorem plycjlem

Proof