Theorem mzpresrename

Description: A polynomial is a polynomial over all larger index sets. (Contributed by Stefan O'Rear, 5-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

	Ref	Expression
Assertion	mzpresrename	⊢ ( ( 𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝑉 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		coires1	⊢ ( 𝑥 ∘ ( I ↾ 𝑉 ) ) = ( 𝑥 ↾ 𝑉 )
2	1	fveq2i	⊢ ( 𝐹 ‘ ( 𝑥 ∘ ( I ↾ 𝑉 ) ) ) = ( 𝐹 ‘ ( 𝑥 ↾ 𝑉 ) )
3	2	mpteq2i	⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ ( I ↾ 𝑉 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝑉 ) ) )
4		simp1	⊢ ( ( 𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝑊 ∈ V )
5		simp3	⊢ ( ( 𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝐹 ∈ ( mzPoly ‘ 𝑉 ) )
6		f1oi	⊢ ( I ↾ 𝑉 ) : 𝑉 –1-1-onto→ 𝑉
7		f1of	⊢ ( ( I ↾ 𝑉 ) : 𝑉 –1-1-onto→ 𝑉 → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 )
8	6 7	ax-mp	⊢ ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉
9		fss	⊢ ( ( ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 ∧ 𝑉 ⊆ 𝑊 ) → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑊 )
10	8 9	mpan	⊢ ( 𝑉 ⊆ 𝑊 → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑊 )
11	10	3ad2ant2	⊢ ( ( 𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑊 )
12		mzprename	⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑊 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ ( I ↾ 𝑉 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
13	4 5 11 12	syl3anc	⊢ ( ( 𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ∘ ( I ↾ 𝑉 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
14	3 13	eqeltrrid	⊢ ( ( 𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝑉 ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )