Theorem mzpresrename

Description: A polynomial is a polynomial over all larger index sets. (Contributed by Stefan O'Rear, 5-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

	Ref	Expression
Assertion	mzpresrename	|- ( ( W e. _V /\ V C_ W /\ F e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x |` V ) ) ) e. ( mzPoly ` W ) )

Proof

Step	Hyp	Ref	Expression
1		coires1	|- ( x o. ( _I |` V ) ) = ( x |` V )
2	1	fveq2i	|- ( F ` ( x o. ( _I |` V ) ) ) = ( F ` ( x |` V ) )
3	2	mpteq2i	|- ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. ( _I |` V ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( F ` ( x |` V ) ) )
4		simp1	|- ( ( W e. _V /\ V C_ W /\ F e. ( mzPoly ` V ) ) -> W e. _V )
5		simp3	|- ( ( W e. _V /\ V C_ W /\ F e. ( mzPoly ` V ) ) -> F e. ( mzPoly ` V ) )
6		f1oi	|- ( _I |` V ) : V -1-1-onto-> V
7		f1of	|- ( ( _I |` V ) : V -1-1-onto-> V -> ( _I |` V ) : V --> V )
8	6 7	ax-mp	|- ( _I |` V ) : V --> V
9		fss	|- ( ( ( _I |` V ) : V --> V /\ V C_ W ) -> ( _I |` V ) : V --> W )
10	8 9	mpan	|- ( V C_ W -> ( _I |` V ) : V --> W )
11	10	3ad2ant2	|- ( ( W e. _V /\ V C_ W /\ F e. ( mzPoly ` V ) ) -> ( _I |` V ) : V --> W )
12		mzprename	|- ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ ( _I |` V ) : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. ( _I |` V ) ) ) ) e. ( mzPoly ` W ) )
13	4 5 11 12	syl3anc	|- ( ( W e. _V /\ V C_ W /\ F e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. ( _I |` V ) ) ) ) e. ( mzPoly ` W ) )
14	3 13	eqeltrrid	|- ( ( W e. _V /\ V C_ W /\ F e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x |` V ) ) ) e. ( mzPoly ` W ) )