plyrecj

Description: A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014)

		Ref	Expression
	Assertion	plyrecj	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to \overline{F (A)} = F (\overline{A})$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to (0 \dots \deg (F)) \in Fin$
2		0re	$⊢ 0 \in ℝ$
3		eqid	$⊢ coeff (F) = coeff (F)$
4	3	coef2	$⊢ (F \in Poly (ℝ) \land 0 \in ℝ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
5	2 4	mpan2	$⊢ F \in Poly (ℝ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
6	5	adantr	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
7		elfznn0	$⊢ x \in (0 \dots \deg (F)) \to x \in ℕ_{0}$
8		ffvelrn	$⊢ (coeff (F) : ℕ_{0} ⟶ ℝ \land x \in ℕ_{0}) \to coeff (F) (x) \in ℝ$
9	6 7 8	syl2an	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to coeff (F) (x) \in ℝ$
10	9	recnd	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to coeff (F) (x) \in ℂ$
11		simpr	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to A \in ℂ$
12		expcl	$⊢ (A \in ℂ \land x \in ℕ_{0}) \to A^{x} \in ℂ$
13	11 7 12	syl2an	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to A^{x} \in ℂ$
14	10 13	mulcld	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to coeff (F) (x) A^{x} \in ℂ$
15	1 14	fsumcj	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to \overline{\sum_{x = 0}^{\deg (F)} coeff (F) (x) A^{x}} = \sum_{x = 0}^{\deg (F)} \overline{coeff (F) (x) A^{x}}$
16	10 13	cjmuld	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to \overline{coeff (F) (x) A^{x}} = \overline{coeff (F) (x)} \overline{A^{x}}$
17	9	cjred	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to \overline{coeff (F) (x)} = coeff (F) (x)$
18		cjexp	$⊢ (A \in ℂ \land x \in ℕ_{0}) \to \overline{A^{x}} = {\overline{A}}^{x}$
19	11 7 18	syl2an	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to \overline{A^{x}} = {\overline{A}}^{x}$
20	17 19	oveq12d	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to \overline{coeff (F) (x)} \overline{A^{x}} = coeff (F) (x) {\overline{A}}^{x}$
21	16 20	eqtrd	$⊢ ((F \in Poly (ℝ) \land A \in ℂ) \land x \in (0 \dots \deg (F))) \to \overline{coeff (F) (x) A^{x}} = coeff (F) (x) {\overline{A}}^{x}$
22	21	sumeq2dv	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to \sum_{x = 0}^{\deg (F)} \overline{coeff (F) (x) A^{x}} = \sum_{x = 0}^{\deg (F)} coeff (F) (x) {\overline{A}}^{x}$
23	15 22	eqtrd	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to \overline{\sum_{x = 0}^{\deg (F)} coeff (F) (x) A^{x}} = \sum_{x = 0}^{\deg (F)} coeff (F) (x) {\overline{A}}^{x}$
24		eqid	$⊢ \deg (F) = \deg (F)$
25	3 24	coeid2	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to F (A) = \sum_{x = 0}^{\deg (F)} coeff (F) (x) A^{x}$
26	25	fveq2d	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to \overline{F (A)} = \overline{\sum_{x = 0}^{\deg (F)} coeff (F) (x) A^{x}}$
27		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
28	3 24	coeid2	$⊢ (F \in Poly (ℝ) \land \overline{A} \in ℂ) \to F (\overline{A}) = \sum_{x = 0}^{\deg (F)} coeff (F) (x) {\overline{A}}^{x}$
29	27 28	sylan2	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to F (\overline{A}) = \sum_{x = 0}^{\deg (F)} coeff (F) (x) {\overline{A}}^{x}$
30	23 26 29	3eqtr4d	$⊢ (F \in Poly (ℝ) \land A \in ℂ) \to \overline{F (A)} = F (\overline{A})$

Metamath Proof Explorer

Theorem plyrecj

Proof