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 ffvelcdm ⊢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∈Vb∈ℤW⟼b⁡R⁡a∈mzPoly⁡W
27 mzpsubst ⊢W∈V∧F∈mzPoly⁡V∧∀a∈Vb∈ℤ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