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 V F mzPoly V R : V W x W F x R mzPoly W

Proof

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