Metamath Proof Explorer

Theorem mzpexpmpt

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

Ref Expression
Assertion mzpexpmpt ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐷 ∈ ℕ0 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝐷 ) ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑎 = 0 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 0 ) )
2 1 mpteq2dv ⊢ ( 𝑎 = 0 → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 0 ) ) )
3 2 eleq1d ⊢ ( 𝑎 = 0 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 0 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) )
4 3 imbi2d ⊢ ( 𝑎 = 0 → ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ↔ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 0 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
5 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 𝑏 ) )
6 5 mpteq2dv ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) )
7 6 eleq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) )
8 7 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ↔ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
9 oveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ ( 𝑏 + 1 ) ) )
10 9 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) )
11 10 eleq1d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) ) )
12 11 imbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ↔ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
13 oveq2 ⊢ ( 𝑎 = 𝐷 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 𝐷 ) )
14 13 mpteq2dv ⊢ ( 𝑎 = 𝐷 → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝐷 ) ) )
15 14 eleq1d ⊢ ( 𝑎 = 𝐷 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝐷 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) )
16 15 imbi2d ⊢ ( 𝑎 = 𝐷 → ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑎 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ↔ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝐷 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
17 mzpf ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
18 zsscn ⊢ ℤ ⊆ ℂ
19 fss ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ℤ ⊆ ℂ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℂ )
20 17 18 19 sylancl ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℂ )
21 eqid ⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 )
22 21 fmpt ⊢ ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℂ )
23 20 22 sylibr ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ )
24 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ
25 rspa ⊢ ( ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝐴 ∈ ℂ )
26 25 exp0d ⊢ ( ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝐴 ↑ 0 ) = 1 )
27 24 26 mpteq2da ⊢ ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 0 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 1 ) )
28 23 27 syl ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 0 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 1 ) )
29 elfvex ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
30 1z ⊢ 1 ∈ ℤ
31 mzpconstmpt ⊢ ( ( 𝑉 ∈ V ∧ 1 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 1 ) ∈ ( mzPoly ‘ 𝑉 ) )
32 29 30 31 sylancl ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 1 ) ∈ ( mzPoly ‘ 𝑉 ) )
33 28 32 eqeltrd ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 0 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
34 23 3ad2ant2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ )
35 simp1 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → 𝑏 ∈ ℕ0 )
36 nfv ⊢ Ⅎ 𝑥 𝑏 ∈ ℕ0
37 24 36 nfan ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0 )
38 25 adantlr ⊢ ( ( ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝐴 ∈ ℂ )
39 simplr ⊢ ( ( ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑏 ∈ ℕ0 )
40 38 39 expp1d ⊢ ( ( ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) = ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) )
41 37 40 mpteq2da ⊢ ( ( ∀ 𝑥 ∈ ( ℤ ↑m 𝑉 ) 𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) ) )
42 34 35 41 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) ) )
43 simp3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
44 simp2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) )
45 mzpmulmpt ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
46 43 44 45 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
47 42 46 eqeltrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) )
48 47 3exp ⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
49 48 a2d ⊢ ( 𝑏 ∈ ℕ0 → ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝑏 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
50 4 8 12 16 33 49 nn0ind ⊢ ( 𝐷 ∈ ℕ0 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝐷 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) )
51 50 impcom ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐷 ∈ ℕ0 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 ↑ 𝐷 ) ) ∈ ( mzPoly ‘ 𝑉 ) )