plyco

Description: The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	plyco.1	$⊢ φ \to F \in Poly (S)$
	plyco.2	$⊢ φ \to G \in Poly (S)$
	plyco.3	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
	plyco.4	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
Assertion	plyco	$⊢ φ \to F \circ G \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		plyco.1	$⊢ φ \to F \in Poly (S)$
2		plyco.2	$⊢ φ \to G \in Poly (S)$
3		plyco.3	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
4		plyco.4	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
5		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
6	2 5	syl	$⊢ φ \to G : ℂ ⟶ ℂ$
7	6	ffvelrnda	$⊢ (φ \land z \in ℂ) \to G (z) \in ℂ$
8	6	feqmptd	$⊢ φ \to G = (z \in ℂ ⟼ G (z))$
9		eqid	$⊢ coeff (F) = coeff (F)$
10		eqid	$⊢ \deg (F) = \deg (F)$
11	9 10	coeid	$⊢ F \in Poly (S) \to F = (x \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) x^{k})$
12	1 11	syl	$⊢ φ \to F = (x \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) x^{k})$
13		oveq1	$⊢ x = G (z) \to x^{k} = {G (z)}^{k}$
14	13	oveq2d	$⊢ x = G (z) \to coeff (F) (k) x^{k} = coeff (F) (k) {G (z)}^{k}$
15	14	sumeq2sdv	$⊢ x = G (z) \to \sum_{k = 0}^{\deg (F)} coeff (F) (k) x^{k} = \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k}$
16	7 8 12 15	fmptco	$⊢ φ \to F \circ G = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k})$
17		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
18	1 17	syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
19		oveq2	$⊢ x = 0 \to (0 \dots x) = (0 \dots 0)$
20	19	sumeq1d	$⊢ x = 0 \to \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k} = \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k}$
21	20	mpteq2dv	$⊢ x = 0 \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k})$
22	21	eleq1d	$⊢ x = 0 \to ((z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
23	22	imbi2d	$⊢ x = 0 \to ((φ \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k}) \in Poly (S)))$
24		oveq2	$⊢ x = d \to (0 \dots x) = (0 \dots d)$
25	24	sumeq1d	$⊢ x = d \to \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k} = \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}$
26	25	mpteq2dv	$⊢ x = d \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k})$
27	26	eleq1d	$⊢ x = d \to ((z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
28	27	imbi2d	$⊢ x = d \to ((φ \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S)))$
29		oveq2	$⊢ x = d + 1 \to (0 \dots x) = (0 \dots d + 1)$
30	29	sumeq1d	$⊢ x = d + 1 \to \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k} = \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}$
31	30	mpteq2dv	$⊢ x = d + 1 \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k})$
32	31	eleq1d	$⊢ x = d + 1 \to ((z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
33	32	imbi2d	$⊢ x = d + 1 \to ((φ \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) \in Poly (S)))$
34		oveq2	$⊢ x = \deg (F) \to (0 \dots x) = (0 \dots \deg (F))$
35	34	sumeq1d	$⊢ x = \deg (F) \to \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k} = \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k}$
36	35	mpteq2dv	$⊢ x = \deg (F) \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k})$
37	36	eleq1d	$⊢ x = \deg (F) \to ((z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
38	37	imbi2d	$⊢ x = \deg (F) \to ((φ \to (z \in ℂ ⟼ \sum_{k = 0}^{x} coeff (F) (k) {G (z)}^{k}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k}) \in Poly (S)))$
39		0z	$⊢ 0 \in ℤ$
40	7	exp0d	$⊢ (φ \land z \in ℂ) \to {G (z)}^{0} = 1$
41	40	oveq2d	$⊢ (φ \land z \in ℂ) \to coeff (F) (0) {G (z)}^{0} = coeff (F) (0) \cdot 1$
42		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
43	1 42	syl	$⊢ φ \to S \subseteq ℂ$
44		0cnd	$⊢ φ \to 0 \in ℂ$
45	44	snssd	$⊢ φ \to \{0\} \subseteq ℂ$
46	43 45	unssd	$⊢ φ \to S \cup \{0\} \subseteq ℂ$
47	9	coef	$⊢ F \in Poly (S) \to coeff (F) : ℕ_{0} ⟶ S \cup \{0\}$
48	1 47	syl	$⊢ φ \to coeff (F) : ℕ_{0} ⟶ S \cup \{0\}$
49		0nn0	$⊢ 0 \in ℕ_{0}$
50		ffvelrn	$⊢ (coeff (F) : ℕ_{0} ⟶ S \cup \{0\} \land 0 \in ℕ_{0}) \to coeff (F) (0) \in (S \cup \{0\})$
51	48 49 50	sylancl	$⊢ φ \to coeff (F) (0) \in (S \cup \{0\})$
52	46 51	sseldd	$⊢ φ \to coeff (F) (0) \in ℂ$
53	52	adantr	$⊢ (φ \land z \in ℂ) \to coeff (F) (0) \in ℂ$
54	53	mulid1d	$⊢ (φ \land z \in ℂ) \to coeff (F) (0) \cdot 1 = coeff (F) (0)$
55	41 54	eqtrd	$⊢ (φ \land z \in ℂ) \to coeff (F) (0) {G (z)}^{0} = coeff (F) (0)$
56	55 53	eqeltrd	$⊢ (φ \land z \in ℂ) \to coeff (F) (0) {G (z)}^{0} \in ℂ$
57		fveq2	$⊢ k = 0 \to coeff (F) (k) = coeff (F) (0)$
58		oveq2	$⊢ k = 0 \to {G (z)}^{k} = {G (z)}^{0}$
59	57 58	oveq12d	$⊢ k = 0 \to coeff (F) (k) {G (z)}^{k} = coeff (F) (0) {G (z)}^{0}$
60	59	fsum1	$⊢ (0 \in ℤ \land coeff (F) (0) {G (z)}^{0} \in ℂ) \to \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k} = coeff (F) (0) {G (z)}^{0}$
61	39 56 60	sylancr	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k} = coeff (F) (0) {G (z)}^{0}$
62	61 55	eqtrd	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k} = coeff (F) (0)$
63	62	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ coeff (F) (0))$
64		fconstmpt	$⊢ ℂ \times \{coeff (F) (0)\} = (z \in ℂ ⟼ coeff (F) (0))$
65	63 64	syl6eqr	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k}) = ℂ \times \{coeff (F) (0)\}$
66		plyconst	$⊢ (S \cup \{0\} \subseteq ℂ \land coeff (F) (0) \in (S \cup \{0\})) \to ℂ \times \{coeff (F) (0)\} \in Poly (S \cup \{0\})$
67	46 51 66	syl2anc	$⊢ φ \to ℂ \times \{coeff (F) (0)\} \in Poly (S \cup \{0\})$
68		plyun0	$⊢ Poly (S \cup \{0\}) = Poly (S)$
69	67 68	eleqtrdi	$⊢ φ \to ℂ \times \{coeff (F) (0)\} \in Poly (S)$
70	65 69	eqeltrd	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{0} coeff (F) (k) {G (z)}^{k}) \in Poly (S)$
71		simprr	$⊢ (φ \land (d \in ℕ_{0} \land (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S))) \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S)$
72	46	adantr	$⊢ (φ \land d \in ℕ_{0}) \to S \cup \{0\} \subseteq ℂ$
73		peano2nn0	$⊢ d \in ℕ_{0} \to d + 1 \in ℕ_{0}$
74		ffvelrn	$⊢ (coeff (F) : ℕ_{0} ⟶ S \cup \{0\} \land d + 1 \in ℕ_{0}) \to coeff (F) (d + 1) \in (S \cup \{0\})$
75	48 73 74	syl2an	$⊢ (φ \land d \in ℕ_{0}) \to coeff (F) (d + 1) \in (S \cup \{0\})$
76		plyconst	$⊢ (S \cup \{0\} \subseteq ℂ \land coeff (F) (d + 1) \in (S \cup \{0\})) \to ℂ \times \{coeff (F) (d + 1)\} \in Poly (S \cup \{0\})$
77	72 75 76	syl2anc	$⊢ (φ \land d \in ℕ_{0}) \to ℂ \times \{coeff (F) (d + 1)\} \in Poly (S \cup \{0\})$
78	77 68	eleqtrdi	$⊢ (φ \land d \in ℕ_{0}) \to ℂ \times \{coeff (F) (d + 1)\} \in Poly (S)$
79		nn0p1nn	$⊢ d \in ℕ_{0} \to d + 1 \in ℕ$
80		oveq2	$⊢ x = 1 \to {G (z)}^{x} = {G (z)}^{1}$
81	80	mpteq2dv	$⊢ x = 1 \to (z \in ℂ ⟼ {G (z)}^{x}) = (z \in ℂ ⟼ {G (z)}^{1})$
82	81	eleq1d	$⊢ x = 1 \to ((z \in ℂ ⟼ {G (z)}^{x}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ {G (z)}^{1}) \in Poly (S))$
83	82	imbi2d	$⊢ x = 1 \to ((φ \to (z \in ℂ ⟼ {G (z)}^{x}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ {G (z)}^{1}) \in Poly (S)))$
84		oveq2	$⊢ x = d \to {G (z)}^{x} = {G (z)}^{d}$
85	84	mpteq2dv	$⊢ x = d \to (z \in ℂ ⟼ {G (z)}^{x}) = (z \in ℂ ⟼ {G (z)}^{d})$
86	85	eleq1d	$⊢ x = d \to ((z \in ℂ ⟼ {G (z)}^{x}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S))$
87	86	imbi2d	$⊢ x = d \to ((φ \to (z \in ℂ ⟼ {G (z)}^{x}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S)))$
88		oveq2	$⊢ x = d + 1 \to {G (z)}^{x} = {G (z)}^{d + 1}$
89	88	mpteq2dv	$⊢ x = d + 1 \to (z \in ℂ ⟼ {G (z)}^{x}) = (z \in ℂ ⟼ {G (z)}^{d + 1})$
90	89	eleq1d	$⊢ x = d + 1 \to ((z \in ℂ ⟼ {G (z)}^{x}) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S))$
91	90	imbi2d	$⊢ x = d + 1 \to ((φ \to (z \in ℂ ⟼ {G (z)}^{x}) \in Poly (S)) \leftrightarrow (φ \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S)))$
92	7	exp1d	$⊢ (φ \land z \in ℂ) \to {G (z)}^{1} = G (z)$
93	92	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ {G (z)}^{1}) = (z \in ℂ ⟼ G (z))$
94	93 8	eqtr4d	$⊢ φ \to (z \in ℂ ⟼ {G (z)}^{1}) = G$
95	94 2	eqeltrd	$⊢ φ \to (z \in ℂ ⟼ {G (z)}^{1}) \in Poly (S)$
96		simprr	$⊢ (φ \land (d \in ℕ \land (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S))) \to (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S)$
97	2	adantr	$⊢ (φ \land (d \in ℕ \land (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S))) \to G \in Poly (S)$
98	3	adantlr	$⊢ ((φ \land (d \in ℕ \land (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S))) \land (x \in S \land y \in S)) \to x + y \in S$
99	4	adantlr	$⊢ ((φ \land (d \in ℕ \land (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S))) \land (x \in S \land y \in S)) \to x y \in S$
100	96 97 98 99	plymul	$⊢ (φ \land (d \in ℕ \land (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S))) \to (z \in ℂ ⟼ {G (z)}^{d}) \times_{f} G \in Poly (S)$
101	100	expr	$⊢ (φ \land d \in ℕ) \to ((z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S) \to (z \in ℂ ⟼ {G (z)}^{d}) \times_{f} G \in Poly (S))$
102		cnex	$⊢ ℂ \in V$
103	102	a1i	$⊢ (φ \land d \in ℕ) \to ℂ \in V$
104		ovexd	$⊢ ((φ \land d \in ℕ) \land z \in ℂ) \to {G (z)}^{d} \in V$
105	7	adantlr	$⊢ ((φ \land d \in ℕ) \land z \in ℂ) \to G (z) \in ℂ$
106		eqidd	$⊢ (φ \land d \in ℕ) \to (z \in ℂ ⟼ {G (z)}^{d}) = (z \in ℂ ⟼ {G (z)}^{d})$
107	8	adantr	$⊢ (φ \land d \in ℕ) \to G = (z \in ℂ ⟼ G (z))$
108	103 104 105 106 107	offval2	$⊢ (φ \land d \in ℕ) \to (z \in ℂ ⟼ {G (z)}^{d}) \times_{f} G = (z \in ℂ ⟼ {G (z)}^{d} G (z))$
109		nnnn0	$⊢ d \in ℕ \to d \in ℕ_{0}$
110	109	ad2antlr	$⊢ ((φ \land d \in ℕ) \land z \in ℂ) \to d \in ℕ_{0}$
111	105 110	expp1d	$⊢ ((φ \land d \in ℕ) \land z \in ℂ) \to {G (z)}^{d + 1} = {G (z)}^{d} G (z)$
112	111	mpteq2dva	$⊢ (φ \land d \in ℕ) \to (z \in ℂ ⟼ {G (z)}^{d + 1}) = (z \in ℂ ⟼ {G (z)}^{d} G (z))$
113	108 112	eqtr4d	$⊢ (φ \land d \in ℕ) \to (z \in ℂ ⟼ {G (z)}^{d}) \times_{f} G = (z \in ℂ ⟼ {G (z)}^{d + 1})$
114	113	eleq1d	$⊢ (φ \land d \in ℕ) \to ((z \in ℂ ⟼ {G (z)}^{d}) \times_{f} G \in Poly (S) \leftrightarrow (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S))$
115	101 114	sylibd	$⊢ (φ \land d \in ℕ) \to ((z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S) \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S))$
116	115	expcom	$⊢ d \in ℕ \to (φ \to ((z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S) \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S)))$
117	116	a2d	$⊢ d \in ℕ \to ((φ \to (z \in ℂ ⟼ {G (z)}^{d}) \in Poly (S)) \to (φ \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S)))$
118	83 87 91 91 95 117	nnind	$⊢ d + 1 \in ℕ \to (φ \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S))$
119	79 118	syl	$⊢ d \in ℕ_{0} \to (φ \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S))$
120	119	impcom	$⊢ (φ \land d \in ℕ_{0}) \to (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S)$
121	3	adantlr	$⊢ ((φ \land d \in ℕ_{0}) \land (x \in S \land y \in S)) \to x + y \in S$
122	4	adantlr	$⊢ ((φ \land d \in ℕ_{0}) \land (x \in S \land y \in S)) \to x y \in S$
123	78 120 121 122	plymul	$⊢ (φ \land d \in ℕ_{0}) \to (ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S)$
124	123	adantrr	$⊢ (φ \land (d \in ℕ_{0} \land (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S))) \to (ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1}) \in Poly (S)$
125	3	adantlr	$⊢ ((φ \land (d \in ℕ_{0} \land (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S))) \land (x \in S \land y \in S)) \to x + y \in S$
126	71 124 125	plyadd	$⊢ (φ \land (d \in ℕ_{0} \land (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S))) \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) +_{f} ((ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1})) \in Poly (S)$
127	126	expr	$⊢ (φ \land d \in ℕ_{0}) \to ((z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) +_{f} ((ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1})) \in Poly (S))$
128	102	a1i	$⊢ (φ \land d \in ℕ_{0}) \to ℂ \in V$
129		sumex	$⊢ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k} \in V$
130	129	a1i	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k} \in V$
131		ovexd	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to coeff (F) (d + 1) {G (z)}^{d + 1} \in V$
132		eqidd	$⊢ (φ \land d \in ℕ_{0}) \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k})$
133		fvexd	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to coeff (F) (d + 1) \in V$
134		ovexd	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to {G (z)}^{d + 1} \in V$
135		fconstmpt	$⊢ ℂ \times \{coeff (F) (d + 1)\} = (z \in ℂ ⟼ coeff (F) (d + 1))$
136	135	a1i	$⊢ (φ \land d \in ℕ_{0}) \to ℂ \times \{coeff (F) (d + 1)\} = (z \in ℂ ⟼ coeff (F) (d + 1))$
137		eqidd	$⊢ (φ \land d \in ℕ_{0}) \to (z \in ℂ ⟼ {G (z)}^{d + 1}) = (z \in ℂ ⟼ {G (z)}^{d + 1})$
138	128 133 134 136 137	offval2	$⊢ (φ \land d \in ℕ_{0}) \to (ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1}) = (z \in ℂ ⟼ coeff (F) (d + 1) {G (z)}^{d + 1})$
139	128 130 131 132 138	offval2	$⊢ (φ \land d \in ℕ_{0}) \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) +_{f} ((ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1})) = (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k} + coeff (F) (d + 1) {G (z)}^{d + 1})$
140		simplr	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to d \in ℕ_{0}$
141		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
142	140 141	eleqtrdi	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to d \in ℤ_{\geq 0}$
143	9	coef3	$⊢ F \in Poly (S) \to coeff (F) : ℕ_{0} ⟶ ℂ$
144	1 143	syl	$⊢ φ \to coeff (F) : ℕ_{0} ⟶ ℂ$
145	144	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to coeff (F) : ℕ_{0} ⟶ ℂ$
146		elfznn0	$⊢ k \in (0 \dots d + 1) \to k \in ℕ_{0}$
147		ffvelrn	$⊢ (coeff (F) : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to coeff (F) (k) \in ℂ$
148	145 146 147	syl2an	$⊢ (((φ \land d \in ℕ_{0}) \land z \in ℂ) \land k \in (0 \dots d + 1)) \to coeff (F) (k) \in ℂ$
149	7	adantlr	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to G (z) \in ℂ$
150		expcl	$⊢ (G (z) \in ℂ \land k \in ℕ_{0}) \to {G (z)}^{k} \in ℂ$
151	149 146 150	syl2an	$⊢ (((φ \land d \in ℕ_{0}) \land z \in ℂ) \land k \in (0 \dots d + 1)) \to {G (z)}^{k} \in ℂ$
152	148 151	mulcld	$⊢ (((φ \land d \in ℕ_{0}) \land z \in ℂ) \land k \in (0 \dots d + 1)) \to coeff (F) (k) {G (z)}^{k} \in ℂ$
153		fveq2	$⊢ k = d + 1 \to coeff (F) (k) = coeff (F) (d + 1)$
154		oveq2	$⊢ k = d + 1 \to {G (z)}^{k} = {G (z)}^{d + 1}$
155	153 154	oveq12d	$⊢ k = d + 1 \to coeff (F) (k) {G (z)}^{k} = coeff (F) (d + 1) {G (z)}^{d + 1}$
156	142 152 155	fsump1	$⊢ ((φ \land d \in ℕ_{0}) \land z \in ℂ) \to \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k} = \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k} + coeff (F) (d + 1) {G (z)}^{d + 1}$
157	156	mpteq2dva	$⊢ (φ \land d \in ℕ_{0}) \to (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k} + coeff (F) (d + 1) {G (z)}^{d + 1})$
158	139 157	eqtr4d	$⊢ (φ \land d \in ℕ_{0}) \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) +_{f} ((ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1})) = (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k})$
159	158	eleq1d	$⊢ (φ \land d \in ℕ_{0}) \to ((z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) +_{f} ((ℂ \times \{coeff (F) (d + 1)\}) \times_{f} (z \in ℂ ⟼ {G (z)}^{d + 1})) \in Poly (S) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
160	127 159	sylibd	$⊢ (φ \land d \in ℕ_{0}) \to ((z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \to (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
161	160	expcom	$⊢ d \in ℕ_{0} \to (φ \to ((z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S) \to (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) \in Poly (S)))$
162	161	a2d	$⊢ d \in ℕ_{0} \to ((φ \to (z \in ℂ ⟼ \sum_{k = 0}^{d} coeff (F) (k) {G (z)}^{k}) \in Poly (S)) \to (φ \to (z \in ℂ ⟼ \sum_{k = 0}^{d + 1} coeff (F) (k) {G (z)}^{k}) \in Poly (S)))$
163	23 28 33 38 70 162	nn0ind	$⊢ \deg (F) \in ℕ_{0} \to (φ \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k}) \in Poly (S))$
164	18 163	mpcom	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (F)} coeff (F) (k) {G (z)}^{k}) \in Poly (S)$
165	16 164	eqeltrd	$⊢ φ \to F \circ G \in Poly (S)$

Metamath Proof Explorer

Theorem plyco

Proof