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 ∈ 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