Metamath Proof Explorer

Theorem mzpcl2

Description: Defining property 2 of a polynomially closed function set P : it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	mzpcl2	$⊢ (P \in mzPolyCld (V) \land F \in V) \to (g \in (ℤ^{V}) ⟼ g (F)) \in P$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (P \in mzPolyCld (V) \land F \in V) \to F \in V$
2		simpl	$⊢ (P \in mzPolyCld (V) \land F \in V) \to P \in mzPolyCld (V)$
3		elfvex	$⊢ P \in mzPolyCld (V) \to V \in V$
4	3	adantr	$⊢ (P \in mzPolyCld (V) \land F \in V) \to V \in V$
5		elmzpcl	$⊢ V \in V \to (P \in mzPolyCld (V) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))))$
6	4 5	syl	$⊢ (P \in mzPolyCld (V) \land F \in V) \to (P \in mzPolyCld (V) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))))$
7	2 6	mpbid	$⊢ (P \in mzPolyCld (V) \land F \in V) \to (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)))$
8		simprlr	$⊢ (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))) \to \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P$
9	7 8	syl	$⊢ (P \in mzPolyCld (V) \land F \in V) \to \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P$
10		fveq2	$⊢ f = F \to g (f) = g (F)$
11	10	mpteq2dv	$⊢ f = F \to (g \in (ℤ^{V}) ⟼ g (f)) = (g \in (ℤ^{V}) ⟼ g (F))$
12	11	eleq1d	$⊢ f = F \to ((g \in (ℤ^{V}) ⟼ g (f)) \in P \leftrightarrow (g \in (ℤ^{V}) ⟼ g (F)) \in P)$
13	12	rspcva	$⊢ (F \in V \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \to (g \in (ℤ^{V}) ⟼ g (F)) \in P$
14	1 9 13	syl2anc	$⊢ (P \in mzPolyCld (V) \land F \in V) \to (g \in (ℤ^{V}) ⟼ g (F)) \in P$