mzpexpmpt

Description: Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014)

		Ref	Expression
	Assertion	mzpexpmpt	$⊢ ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land D \in ℕ_{0}) \to (x \in (ℤ^{V}) ⟼ A^{D}) \in mzPoly (V)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ a = 0 \to A^{a} = A^{0}$
2	1	mpteq2dv	$⊢ a = 0 \to (x \in (ℤ^{V}) ⟼ A^{a}) = (x \in (ℤ^{V}) ⟼ A^{0})$
3	2	eleq1d	$⊢ a = 0 \to ((x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V) \leftrightarrow (x \in (ℤ^{V}) ⟼ A^{0}) \in mzPoly (V))$
4	3	imbi2d	$⊢ a = 0 \to (((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V)) \leftrightarrow ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{0}) \in mzPoly (V)))$
5		oveq2	$⊢ a = b \to A^{a} = A^{b}$
6	5	mpteq2dv	$⊢ a = b \to (x \in (ℤ^{V}) ⟼ A^{a}) = (x \in (ℤ^{V}) ⟼ A^{b})$
7	6	eleq1d	$⊢ a = b \to ((x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V) \leftrightarrow (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V))$
8	7	imbi2d	$⊢ a = b \to (((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V)) \leftrightarrow ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)))$
9		oveq2	$⊢ a = b + 1 \to A^{a} = A^{b + 1}$
10	9	mpteq2dv	$⊢ a = b + 1 \to (x \in (ℤ^{V}) ⟼ A^{a}) = (x \in (ℤ^{V}) ⟼ A^{b + 1})$
11	10	eleq1d	$⊢ a = b + 1 \to ((x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V) \leftrightarrow (x \in (ℤ^{V}) ⟼ A^{b + 1}) \in mzPoly (V))$
12	11	imbi2d	$⊢ a = b + 1 \to (((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V)) \leftrightarrow ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{b + 1}) \in mzPoly (V)))$
13		oveq2	$⊢ a = D \to A^{a} = A^{D}$
14	13	mpteq2dv	$⊢ a = D \to (x \in (ℤ^{V}) ⟼ A^{a}) = (x \in (ℤ^{V}) ⟼ A^{D})$
15	14	eleq1d	$⊢ a = D \to ((x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V) \leftrightarrow (x \in (ℤ^{V}) ⟼ A^{D}) \in mzPoly (V))$
16	15	imbi2d	$⊢ a = D \to (((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{a}) \in mzPoly (V)) \leftrightarrow ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{D}) \in mzPoly (V)))$
17		mzpf	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A) : ℤ^{V} ⟶ ℤ$
18		zsscn	$⊢ ℤ \subseteq ℂ$
19		fss	$⊢ ((x \in (ℤ^{V}) ⟼ A) : ℤ^{V} ⟶ ℤ \land ℤ \subseteq ℂ) \to (x \in (ℤ^{V}) ⟼ A) : ℤ^{V} ⟶ ℂ$
20	17 18 19	sylancl	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A) : ℤ^{V} ⟶ ℂ$
21		eqid	$⊢ (x \in (ℤ^{V}) ⟼ A) = (x \in (ℤ^{V}) ⟼ A)$
22	21	fmpt	$⊢ \forall x \in (ℤ^{V}) A \in ℂ \leftrightarrow (x \in (ℤ^{V}) ⟼ A) : ℤ^{V} ⟶ ℂ$
23	20 22	sylibr	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to \forall x \in (ℤ^{V}) A \in ℂ$
24		nfra1	$⊢ Ⅎ x \forall x \in (ℤ^{V}) A \in ℂ$
25		rspa	$⊢ (\forall x \in (ℤ^{V}) A \in ℂ \land x \in (ℤ^{V})) \to A \in ℂ$
26	25	exp0d	$⊢ (\forall x \in (ℤ^{V}) A \in ℂ \land x \in (ℤ^{V})) \to A^{0} = 1$
27	24 26	mpteq2da	$⊢ \forall x \in (ℤ^{V}) A \in ℂ \to (x \in (ℤ^{V}) ⟼ A^{0}) = (x \in (ℤ^{V}) ⟼ 1)$
28	23 27	syl	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{0}) = (x \in (ℤ^{V}) ⟼ 1)$
29		elfvex	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to V \in V$
30		1z	$⊢ 1 \in ℤ$
31		mzpconstmpt	$⊢ (V \in V \land 1 \in ℤ) \to (x \in (ℤ^{V}) ⟼ 1) \in mzPoly (V)$
32	29 30 31	sylancl	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ 1) \in mzPoly (V)$
33	28 32	eqeltrd	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{0}) \in mzPoly (V)$
34	23	3ad2ant2	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to \forall x \in (ℤ^{V}) A \in ℂ$
35		simp1	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to b \in ℕ_{0}$
36		nfv	$⊢ Ⅎ x b \in ℕ_{0}$
37	24 36	nfan	$⊢ Ⅎ x (\forall x \in (ℤ^{V}) A \in ℂ \land b \in ℕ_{0})$
38	25	adantlr	$⊢ ((\forall x \in (ℤ^{V}) A \in ℂ \land b \in ℕ_{0}) \land x \in (ℤ^{V})) \to A \in ℂ$
39		simplr	$⊢ ((\forall x \in (ℤ^{V}) A \in ℂ \land b \in ℕ_{0}) \land x \in (ℤ^{V})) \to b \in ℕ_{0}$
40	38 39	expp1d	$⊢ ((\forall x \in (ℤ^{V}) A \in ℂ \land b \in ℕ_{0}) \land x \in (ℤ^{V})) \to A^{b + 1} = A^{b} A$
41	37 40	mpteq2da	$⊢ (\forall x \in (ℤ^{V}) A \in ℂ \land b \in ℕ_{0}) \to (x \in (ℤ^{V}) ⟼ A^{b + 1}) = (x \in (ℤ^{V}) ⟼ A^{b} A)$
42	34 35 41	syl2anc	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A^{b + 1}) = (x \in (ℤ^{V}) ⟼ A^{b} A)$
43		simp3	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)$
44		simp2	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V)$
45		mzpmulmpt	$⊢ ((x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A^{b} A) \in mzPoly (V)$
46	43 44 45	syl2anc	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A^{b} A) \in mzPoly (V)$
47	42 46	eqeltrd	$⊢ (b \in ℕ_{0} \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A^{b + 1}) \in mzPoly (V)$
48	47	3exp	$⊢ b \in ℕ_{0} \to ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to ((x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{b + 1}) \in mzPoly (V)))$
49	48	a2d	$⊢ b \in ℕ_{0} \to (((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{b}) \in mzPoly (V)) \to ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{b + 1}) \in mzPoly (V)))$
50	4 8 12 16 33 49	nn0ind	$⊢ D \in ℕ_{0} \to ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A^{D}) \in mzPoly (V))$
51	50	impcom	$⊢ ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land D \in ℕ_{0}) \to (x \in (ℤ^{V}) ⟼ A^{D}) \in mzPoly (V)$

Metamath Proof Explorer

Theorem mzpexpmpt

Proof