mzpclall

Description: The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	mzpclall	$⊢ V \in V \to ℤ^{(ℤ^{V})} \in mzPolyCld (V)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ v = V \to ℤ^{v} = ℤ^{V}$
2	1	oveq2d	$⊢ v = V \to ℤ^{(ℤ^{v})} = ℤ^{(ℤ^{V})}$
3		fveq2	$⊢ v = V \to mzPolyCld (v) = mzPolyCld (V)$
4	2 3	eleq12d	$⊢ v = V \to (ℤ^{(ℤ^{v})} \in mzPolyCld (v) \leftrightarrow ℤ^{(ℤ^{V})} \in mzPolyCld (V))$
5		ssid	$⊢ ℤ^{(ℤ^{v})} \subseteq ℤ^{(ℤ^{v})}$
6		ovex	$⊢ ℤ^{v} \in V$
7		zex	$⊢ ℤ \in V$
8	6 7	constmap	$⊢ f \in ℤ \to (ℤ^{v}) \times \{f\} \in (ℤ^{(ℤ^{v})})$
9	8	rgen	$⊢ \forall f \in ℤ (ℤ^{v}) \times \{f\} \in (ℤ^{(ℤ^{v})})$
10		vex	$⊢ v \in V$
11	7 10	elmap	$⊢ g \in (ℤ^{v}) \leftrightarrow g : v ⟶ ℤ$
12		ffvelrn	$⊢ (g : v ⟶ ℤ \land f \in v) \to g (f) \in ℤ$
13	11 12	sylanb	$⊢ (g \in (ℤ^{v}) \land f \in v) \to g (f) \in ℤ$
14	13	ancoms	$⊢ (f \in v \land g \in (ℤ^{v})) \to g (f) \in ℤ$
15	14	fmpttd	$⊢ f \in v \to (g \in (ℤ^{v}) ⟼ g (f)) : ℤ^{v} ⟶ ℤ$
16	7 6	elmap	$⊢ (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})}) \leftrightarrow (g \in (ℤ^{v}) ⟼ g (f)) : ℤ^{v} ⟶ ℤ$
17	15 16	sylibr	$⊢ f \in v \to (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})})$
18	17	rgen	$⊢ \forall f \in v (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})})$
19	9 18	pm3.2i	$⊢ (\forall f \in ℤ (ℤ^{v}) \times \{f\} \in (ℤ^{(ℤ^{v})}) \land \forall f \in v (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})}))$
20		zaddcl	$⊢ (a \in ℤ \land b \in ℤ) \to a + b \in ℤ$
21	20	adantl	$⊢ ((f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \land (a \in ℤ \land b \in ℤ)) \to a + b \in ℤ$
22		simpl	$⊢ (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \to f : ℤ^{v} ⟶ ℤ$
23		simpr	$⊢ (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \to g : ℤ^{v} ⟶ ℤ$
24		ovexd	$⊢ (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \to ℤ^{v} \in V$
25		inidm	$⊢ (ℤ^{v}) \cap (ℤ^{v}) = ℤ^{v}$
26	21 22 23 24 24 25	off	$⊢ (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \to (f +_{f} g) : ℤ^{v} ⟶ ℤ$
27		zmulcl	$⊢ (a \in ℤ \land b \in ℤ) \to a b \in ℤ$
28	27	adantl	$⊢ ((f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \land (a \in ℤ \land b \in ℤ)) \to a b \in ℤ$
29	28 22 23 24 24 25	off	$⊢ (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \to (f \times_{f} g) : ℤ^{v} ⟶ ℤ$
30	26 29	jca	$⊢ (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ) \to ((f +_{f} g) : ℤ^{v} ⟶ ℤ \land (f \times_{f} g) : ℤ^{v} ⟶ ℤ)$
31	7 6	elmap	$⊢ f \in (ℤ^{(ℤ^{v})}) \leftrightarrow f : ℤ^{v} ⟶ ℤ$
32	7 6	elmap	$⊢ g \in (ℤ^{(ℤ^{v})}) \leftrightarrow g : ℤ^{v} ⟶ ℤ$
33	31 32	anbi12i	$⊢ (f \in (ℤ^{(ℤ^{v})}) \land g \in (ℤ^{(ℤ^{v})})) \leftrightarrow (f : ℤ^{v} ⟶ ℤ \land g : ℤ^{v} ⟶ ℤ)$
34	7 6	elmap	$⊢ f +_{f} g \in (ℤ^{(ℤ^{v})}) \leftrightarrow (f +_{f} g) : ℤ^{v} ⟶ ℤ$
35	7 6	elmap	$⊢ f \times_{f} g \in (ℤ^{(ℤ^{v})}) \leftrightarrow (f \times_{f} g) : ℤ^{v} ⟶ ℤ$
36	34 35	anbi12i	$⊢ (f +_{f} g \in (ℤ^{(ℤ^{v})}) \land f \times_{f} g \in (ℤ^{(ℤ^{v})})) \leftrightarrow ((f +_{f} g) : ℤ^{v} ⟶ ℤ \land (f \times_{f} g) : ℤ^{v} ⟶ ℤ)$
37	30 33 36	3imtr4i	$⊢ (f \in (ℤ^{(ℤ^{v})}) \land g \in (ℤ^{(ℤ^{v})})) \to (f +_{f} g \in (ℤ^{(ℤ^{v})}) \land f \times_{f} g \in (ℤ^{(ℤ^{v})}))$
38	37	rgen2	$⊢ \forall f \in (ℤ^{(ℤ^{v})}) \forall g \in (ℤ^{(ℤ^{v})}) (f +_{f} g \in (ℤ^{(ℤ^{v})}) \land f \times_{f} g \in (ℤ^{(ℤ^{v})}))$
39	19 38	pm3.2i	$⊢ ((\forall f \in ℤ (ℤ^{v}) \times \{f\} \in (ℤ^{(ℤ^{v})}) \land \forall f \in v (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})})) \land \forall f \in (ℤ^{(ℤ^{v})}) \forall g \in (ℤ^{(ℤ^{v})}) (f +_{f} g \in (ℤ^{(ℤ^{v})}) \land f \times_{f} g \in (ℤ^{(ℤ^{v})})))$
40		elmzpcl	$⊢ v \in V \to (ℤ^{(ℤ^{v})} \in mzPolyCld (v) \leftrightarrow (ℤ^{(ℤ^{v})} \subseteq ℤ^{(ℤ^{v})} \land ((\forall f \in ℤ (ℤ^{v}) \times \{f\} \in (ℤ^{(ℤ^{v})}) \land \forall f \in v (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})})) \land \forall f \in (ℤ^{(ℤ^{v})}) \forall g \in (ℤ^{(ℤ^{v})}) (f +_{f} g \in (ℤ^{(ℤ^{v})}) \land f \times_{f} g \in (ℤ^{(ℤ^{v})})))))$
41	10 40	ax-mp	$⊢ ℤ^{(ℤ^{v})} \in mzPolyCld (v) \leftrightarrow (ℤ^{(ℤ^{v})} \subseteq ℤ^{(ℤ^{v})} \land ((\forall f \in ℤ (ℤ^{v}) \times \{f\} \in (ℤ^{(ℤ^{v})}) \land \forall f \in v (g \in (ℤ^{v}) ⟼ g (f)) \in (ℤ^{(ℤ^{v})})) \land \forall f \in (ℤ^{(ℤ^{v})}) \forall g \in (ℤ^{(ℤ^{v})}) (f +_{f} g \in (ℤ^{(ℤ^{v})}) \land f \times_{f} g \in (ℤ^{(ℤ^{v})}))))$
42	5 39 41	mpbir2an	$⊢ ℤ^{(ℤ^{v})} \in mzPolyCld (v)$
43	4 42	vtoclg	$⊢ V \in V \to ℤ^{(ℤ^{V})} \in mzPolyCld (V)$

Metamath Proof Explorer

Theorem mzpclall

Proof