Metamath Proof Explorer

Theorem mzprename

Description: Simplified version of mzpsubst to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzprename 
|- ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. R ) ) ) e. ( mzPoly ` W ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> x e. ( ZZ ^m W ) )
2 zex 
 |-  ZZ e. _V
3 simpll 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> W e. _V )
4 elmapg 
 |-  ( ( ZZ e. _V /\ W e. _V ) -> ( x e. ( ZZ ^m W ) <-> x : W --> ZZ ) )
5 2 3 4 sylancr 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> ( x e. ( ZZ ^m W ) <-> x : W --> ZZ ) )
6 1 5 mpbid 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> x : W --> ZZ )
7 simplr 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> R : V --> W )
8 fcompt 
 |-  ( ( x : W --> ZZ /\ R : V --> W ) -> ( x o. R ) = ( a e. V |-> ( x ` ( R ` a ) ) ) )
9 6 7 8 syl2anc 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> ( x o. R ) = ( a e. V |-> ( x ` ( R ` a ) ) ) )
10 fveq1 
 |-  ( b = x -> ( b ` ( R ` a ) ) = ( x ` ( R ` a ) ) )
11 eqid 
 |-  ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) = ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) )
12 fvex 
 |-  ( x ` ( R ` a ) ) e. _V
13 10 11 12 fvmpt 
 |-  ( x e. ( ZZ ^m W ) -> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) = ( x ` ( R ` a ) ) )
14 13 ad2antlr 
 |-  ( ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) /\ a e. V ) -> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) = ( x ` ( R ` a ) ) )
15 14 eqcomd 
 |-  ( ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) /\ a e. V ) -> ( x ` ( R ` a ) ) = ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) )
16 15 mpteq2dva 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> ( a e. V |-> ( x ` ( R ` a ) ) ) = ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) )
17 9 16 eqtrd 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> ( x o. R ) = ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) )
18 17 fveq2d 
 |-  ( ( ( W e. _V /\ R : V --> W ) /\ x e. ( ZZ ^m W ) ) -> ( F ` ( x o. R ) ) = ( F ` ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) ) )
19 18 mpteq2dva 
 |-  ( ( W e. _V /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. R ) ) ) = ( x e. ( ZZ ^m W ) |-> ( F ` ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) ) ) )
20 19 3adant2 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. R ) ) ) = ( x e. ( ZZ ^m W ) |-> ( F ` ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) ) ) )
21 simpl1 
 |-  ( ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) /\ a e. V ) -> W e. _V )
22 ffvelrn 
 |-  ( ( R : V --> W /\ a e. V ) -> ( R ` a ) e. W )
23 22 3ad2antl3 
 |-  ( ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) /\ a e. V ) -> ( R ` a ) e. W )
24 mzpproj 
 |-  ( ( W e. _V /\ ( R ` a ) e. W ) -> ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) e. ( mzPoly ` W ) )
25 21 23 24 syl2anc 
 |-  ( ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) /\ a e. V ) -> ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) e. ( mzPoly ` W ) )
26 25 ralrimiva 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) -> A. a e. V ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) e. ( mzPoly ` W ) )
27 mzpsubst 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. a e. V ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) e. ( mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) ) ) e. ( mzPoly ` W ) )
28 26 27 syld3an3 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( a e. V |-> ( ( b e. ( ZZ ^m W ) |-> ( b ` ( R ` a ) ) ) ` x ) ) ) ) e. ( mzPoly ` W ) )
29 20 28 eqeltrd 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. R ) ) ) e. ( mzPoly ` W ) )