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	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑅 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑥 ∈ ( ℤ ↑m 𝑊 ) )
2		zex	⊢ ℤ ∈ V
3		simpll	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑊 ∈ V )
4		elmapg	⊢ ( ( ℤ ∈ V ∧ 𝑊 ∈ V ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↔ 𝑥 : 𝑊 ⟶ ℤ ) )
5	2 3 4	sylancr	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↔ 𝑥 : 𝑊 ⟶ ℤ ) )
6	1 5	mpbid	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑥 : 𝑊 ⟶ ℤ )
7		simplr	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑅 : 𝑉 ⟶ 𝑊 )
8		fcompt	⊢ ( ( 𝑥 : 𝑊 ⟶ ℤ ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∘ 𝑅 ) = ( 𝑎 ∈ 𝑉 ↦ ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
9	6 7 8	syl2anc	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑥 ∘ 𝑅 ) = ( 𝑎 ∈ 𝑉 ↦ ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
10		fveq1	⊢ ( 𝑏 = 𝑥 → ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) = ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) )
11		eqid	⊢ ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) = ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) )
12		fvex	⊢ ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) ∈ V
13	10 11 12	fvmpt	⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) → ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) = ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) )
14	13	ad2antlr	⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) = ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) )
15	14	eqcomd	⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) ∧ 𝑎 ∈ 𝑉 ) → ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) = ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) )
16	15	mpteq2dva	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑎 ∈ 𝑉 ↦ ( 𝑥 ‘ ( 𝑅 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) )
17	9 16	eqtrd	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑥 ∘ 𝑅 ) = ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) )
18	17	fveq2d	⊢ ( ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝐹 ‘ ( 𝑥 ∘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) ) )
19	18	mpteq2dva	⊢ ( ( 𝑊 ∈ V ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑅 ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) ) ) )
20	19	3adant2	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑅 ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) ) ) )
21		simpl1	⊢ ( ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑎 ∈ 𝑉 ) → 𝑊 ∈ V )
22		ffvelrn	⊢ ( ( 𝑅 : 𝑉 ⟶ 𝑊 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑅 ‘ 𝑎 ) ∈ 𝑊 )
23	22	3ad2antl3	⊢ ( ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑎 ∈ 𝑉 ) → ( 𝑅 ‘ 𝑎 ) ∈ 𝑊 )
24		mzpproj	⊢ ( ( 𝑊 ∈ V ∧ ( 𝑅 ‘ 𝑎 ) ∈ 𝑊 ) → ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
25	21 23 24	syl2anc	⊢ ( ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) ∧ 𝑎 ∈ 𝑉 ) → ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
26	25	ralrimiva	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ∀ 𝑎 ∈ 𝑉 ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
27		mzpsubst	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
28	26 27	syld3an3	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑎 ∈ 𝑉 ↦ ( ( 𝑏 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑅 ‘ 𝑎 ) ) ) ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
29	20 28	eqeltrd	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝑅 : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ 𝑅 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )