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 
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ D e. NN0 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. ( mzPoly ` V ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = 0 -> ( A ^ a ) = ( A ^ 0 ) )
2 1 mpteq2dv 
 |-  ( a = 0 -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) = ( x e. ( ZZ ^m V ) |-> ( A ^ 0 ) ) )
3 2 eleq1d 
 |-  ( a = 0 -> ( ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) <-> ( x e. ( ZZ ^m V ) |-> ( A ^ 0 ) ) e. ( mzPoly ` V ) ) )
4 3 imbi2d 
 |-  ( a = 0 -> ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) ) <-> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ 0 ) ) e. ( mzPoly ` V ) ) ) )
5 oveq2 
 |-  ( a = b -> ( A ^ a ) = ( A ^ b ) )
6 5 mpteq2dv 
 |-  ( a = b -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) = ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) )
7 6 eleq1d 
 |-  ( a = b -> ( ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) <-> ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) )
8 7 imbi2d 
 |-  ( a = b -> ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) ) <-> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) ) )
9 oveq2 
 |-  ( a = ( b + 1 ) -> ( A ^ a ) = ( A ^ ( b + 1 ) ) )
10 9 mpteq2dv 
 |-  ( a = ( b + 1 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) = ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) )
11 10 eleq1d 
 |-  ( a = ( b + 1 ) -> ( ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) <-> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) e. ( mzPoly ` V ) ) )
12 11 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) ) <-> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) e. ( mzPoly ` V ) ) ) )
13 oveq2 
 |-  ( a = D -> ( A ^ a ) = ( A ^ D ) )
14 13 mpteq2dv 
 |-  ( a = D -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) = ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) )
15 14 eleq1d 
 |-  ( a = D -> ( ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) <-> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. ( mzPoly ` V ) ) )
16 15 imbi2d 
 |-  ( a = D -> ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ a ) ) e. ( mzPoly ` V ) ) <-> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. ( mzPoly ` V ) ) ) )
17 mzpf 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> ZZ )
18 zsscn 
 |-  ZZ C_ CC
19 fss 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> ZZ /\ ZZ C_ CC ) -> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> CC )
20 17 18 19 sylancl 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> CC )
21 eqid 
 |-  ( x e. ( ZZ ^m V ) |-> A ) = ( x e. ( ZZ ^m V ) |-> A )
22 21 fmpt 
 |-  ( A. x e. ( ZZ ^m V ) A e. CC <-> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> CC )
23 20 22 sylibr 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> A. x e. ( ZZ ^m V ) A e. CC )
24 nfra1 
 |-  F/ x A. x e. ( ZZ ^m V ) A e. CC
25 rspa 
 |-  ( ( A. x e. ( ZZ ^m V ) A e. CC /\ x e. ( ZZ ^m V ) ) -> A e. CC )
26 25 exp0d 
 |-  ( ( A. x e. ( ZZ ^m V ) A e. CC /\ x e. ( ZZ ^m V ) ) -> ( A ^ 0 ) = 1 )
27 24 26 mpteq2da 
 |-  ( A. x e. ( ZZ ^m V ) A e. CC -> ( x e. ( ZZ ^m V ) |-> ( A ^ 0 ) ) = ( x e. ( ZZ ^m V ) |-> 1 ) )
28 23 27 syl 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ 0 ) ) = ( x e. ( ZZ ^m V ) |-> 1 ) )
29 elfvex 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> V e. _V )
30 1z 
 |-  1 e. ZZ
31 mzpconstmpt 
 |-  ( ( V e. _V /\ 1 e. ZZ ) -> ( x e. ( ZZ ^m V ) |-> 1 ) e. ( mzPoly ` V ) )
32 29 30 31 sylancl 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> 1 ) e. ( mzPoly ` V ) )
33 28 32 eqeltrd 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ 0 ) ) e. ( mzPoly ` V ) )
34 23 3ad2ant2 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> A. x e. ( ZZ ^m V ) A e. CC )
35 simp1 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> b e. NN0 )
36 nfv 
 |-  F/ x b e. NN0
37 24 36 nfan 
 |-  F/ x ( A. x e. ( ZZ ^m V ) A e. CC /\ b e. NN0 )
38 25 adantlr 
 |-  ( ( ( A. x e. ( ZZ ^m V ) A e. CC /\ b e. NN0 ) /\ x e. ( ZZ ^m V ) ) -> A e. CC )
39 simplr 
 |-  ( ( ( A. x e. ( ZZ ^m V ) A e. CC /\ b e. NN0 ) /\ x e. ( ZZ ^m V ) ) -> b e. NN0 )
40 38 39 expp1d 
 |-  ( ( ( A. x e. ( ZZ ^m V ) A e. CC /\ b e. NN0 ) /\ x e. ( ZZ ^m V ) ) -> ( A ^ ( b + 1 ) ) = ( ( A ^ b ) x. A ) )
41 37 40 mpteq2da 
 |-  ( ( A. x e. ( ZZ ^m V ) A e. CC /\ b e. NN0 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) = ( x e. ( ZZ ^m V ) |-> ( ( A ^ b ) x. A ) ) )
42 34 35 41 syl2anc 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) = ( x e. ( ZZ ^m V ) |-> ( ( A ^ b ) x. A ) ) )
43 simp3 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) )
44 simp2 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) )
45 mzpmulmpt 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( ( A ^ b ) x. A ) ) e. ( mzPoly ` V ) )
46 43 44 45 syl2anc 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( ( A ^ b ) x. A ) ) e. ( mzPoly ` V ) )
47 42 46 eqeltrd 
 |-  ( ( b e. NN0 /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) e. ( mzPoly ` V ) )
48 47 3exp 
 |-  ( b e. NN0 -> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) e. ( mzPoly ` V ) ) ) )
49 48 a2d 
 |-  ( b e. NN0 -> ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ b ) ) e. ( mzPoly ` V ) ) -> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ ( b + 1 ) ) ) e. ( mzPoly ` V ) ) ) )
50 4 8 12 16 33 49 nn0ind 
 |-  ( D e. NN0 -> ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. ( mzPoly ` V ) ) )
51 50 impcom 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ D e. NN0 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. ( mzPoly ` V ) )