Metamath Proof Explorer

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	$⊢ (W \in V \land V \subseteq W \land F \in mzPoly (V)) \to (x \in (ℤ^{W}) ⟼ F ({x ↾}_{V})) \in mzPoly (W)$

Proof

Step	Hyp	Ref	Expression
1		coires1	$⊢ x \circ ({I ↾}_{V}) = {x ↾}_{V}$
2	1	fveq2i	$⊢ F (x \circ ({I ↾}_{V})) = F ({x ↾}_{V})$
3	2	mpteq2i	$⊢ (x \in (ℤ^{W}) ⟼ F (x \circ ({I ↾}_{V}))) = (x \in (ℤ^{W}) ⟼ F ({x ↾}_{V}))$
4		simp1	$⊢ (W \in V \land V \subseteq W \land F \in mzPoly (V)) \to W \in V$
5		simp3	$⊢ (W \in V \land V \subseteq W \land F \in mzPoly (V)) \to F \in mzPoly (V)$
6		f1oi	$⊢ ({I ↾}_{V}) : V \underset{1-1 onto}{⟶} V$
7		f1of	$⊢ ({I ↾}_{V}) : V \underset{1-1 onto}{⟶} V \to ({I ↾}_{V}) : V ⟶ V$
8	6 7	ax-mp	$⊢ ({I ↾}_{V}) : V ⟶ V$
9		fss	$⊢ (({I ↾}_{V}) : V ⟶ V \land V \subseteq W) \to ({I ↾}_{V}) : V ⟶ W$
10	8 9	mpan	$⊢ V \subseteq W \to ({I ↾}_{V}) : V ⟶ W$
11	10	3ad2ant2	$⊢ (W \in V \land V \subseteq W \land F \in mzPoly (V)) \to ({I ↾}_{V}) : V ⟶ W$
12		mzprename	$⊢ (W \in V \land F \in mzPoly (V) \land ({I ↾}_{V}) : V ⟶ W) \to (x \in (ℤ^{W}) ⟼ F (x \circ ({I ↾}_{V}))) \in mzPoly (W)$
13	4 5 11 12	syl3anc	$⊢ (W \in V \land V \subseteq W \land F \in mzPoly (V)) \to (x \in (ℤ^{W}) ⟼ F (x \circ ({I ↾}_{V}))) \in mzPoly (W)$
14	3 13	eqeltrrid	$⊢ (W \in V \land V \subseteq W \land F \in mzPoly (V)) \to (x \in (ℤ^{W}) ⟼ F ({x ↾}_{V})) \in mzPoly (W)$