mzpmfp

Description: Relationship between multivariate Z-polynomials and general multivariate polynomial functions. (Contributed by Stefan O'Rear, 20-Mar-2015) (Revised by AV, 13-Jun-2019)

		Ref	Expression
	Assertion	mzpmfp	$⊢ mzPoly (I) = ran (I eval ℤ_{ring})$

Proof

Step	Hyp	Ref	Expression
1		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
2		eqid	$⊢ I eval ℤ_{ring} = I eval ℤ_{ring}$
3	2 1	evlval	$⊢ I eval ℤ_{ring} = (I evalSub ℤ_{ring}) (ℤ)$
4	3	rneqi	$⊢ ran (I eval ℤ_{ring}) = ran (I evalSub ℤ_{ring}) (ℤ)$
5		simpl	$⊢ (I \in V \land f \in ℤ) \to I \in V$
6		zringcrng	$⊢ ℤ_{ring} \in CRing$
7	6	a1i	$⊢ (I \in V \land f \in ℤ) \to ℤ_{ring} \in CRing$
8		zringring	$⊢ ℤ_{ring} \in Ring$
9	1	subrgid	$⊢ ℤ_{ring} \in Ring \to ℤ \in SubRing (ℤ_{ring})$
10	8 9	ax-mp	$⊢ ℤ \in SubRing (ℤ_{ring})$
11	10	a1i	$⊢ (I \in V \land f \in ℤ) \to ℤ \in SubRing (ℤ_{ring})$
12		simpr	$⊢ (I \in V \land f \in ℤ) \to f \in ℤ$
13	1 4 5 7 11 12	mpfconst	$⊢ (I \in V \land f \in ℤ) \to (ℤ^{I}) \times \{f\} \in ran (I eval ℤ_{ring})$
14		simpl	$⊢ (I \in V \land f \in I) \to I \in V$
15	6	a1i	$⊢ (I \in V \land f \in I) \to ℤ_{ring} \in CRing$
16	10	a1i	$⊢ (I \in V \land f \in I) \to ℤ \in SubRing (ℤ_{ring})$
17		simpr	$⊢ (I \in V \land f \in I) \to f \in I$
18	1 4 14 15 16 17	mpfproj	$⊢ (I \in V \land f \in I) \to (g \in (ℤ^{I}) ⟼ g (f)) \in ran (I eval ℤ_{ring})$
19		simp2r	$⊢ (I \in V \land (f : ℤ^{I} ⟶ ℤ \land f \in ran (I eval ℤ_{ring})) \land (g : ℤ^{I} ⟶ ℤ \land g \in ran (I eval ℤ_{ring}))) \to f \in ran (I eval ℤ_{ring})$
20		simp3r	$⊢ (I \in V \land (f : ℤ^{I} ⟶ ℤ \land f \in ran (I eval ℤ_{ring})) \land (g : ℤ^{I} ⟶ ℤ \land g \in ran (I eval ℤ_{ring}))) \to g \in ran (I eval ℤ_{ring})$
21		zringplusg	$⊢ + = +_{ℤ_{ring}}$
22	4 21	mpfaddcl	$⊢ (f \in ran (I eval ℤ_{ring}) \land g \in ran (I eval ℤ_{ring})) \to f +_{f} g \in ran (I eval ℤ_{ring})$
23	19 20 22	syl2anc	$⊢ (I \in V \land (f : ℤ^{I} ⟶ ℤ \land f \in ran (I eval ℤ_{ring})) \land (g : ℤ^{I} ⟶ ℤ \land g \in ran (I eval ℤ_{ring}))) \to f +_{f} g \in ran (I eval ℤ_{ring})$
24		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
25	4 24	mpfmulcl	$⊢ (f \in ran (I eval ℤ_{ring}) \land g \in ran (I eval ℤ_{ring})) \to f \times_{f} g \in ran (I eval ℤ_{ring})$
26	19 20 25	syl2anc	$⊢ (I \in V \land (f : ℤ^{I} ⟶ ℤ \land f \in ran (I eval ℤ_{ring})) \land (g : ℤ^{I} ⟶ ℤ \land g \in ran (I eval ℤ_{ring}))) \to f \times_{f} g \in ran (I eval ℤ_{ring})$
27		eleq1	$⊢ b = (ℤ^{I}) \times \{f\} \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow (ℤ^{I}) \times \{f\} \in ran (I eval ℤ_{ring}))$
28		eleq1	$⊢ b = (g \in (ℤ^{I}) ⟼ g (f)) \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow (g \in (ℤ^{I}) ⟼ g (f)) \in ran (I eval ℤ_{ring}))$
29		eleq1	$⊢ b = f \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow f \in ran (I eval ℤ_{ring}))$
30		eleq1	$⊢ b = g \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow g \in ran (I eval ℤ_{ring}))$
31		eleq1	$⊢ b = f +_{f} g \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow f +_{f} g \in ran (I eval ℤ_{ring}))$
32		eleq1	$⊢ b = f \times_{f} g \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow f \times_{f} g \in ran (I eval ℤ_{ring}))$
33		eleq1	$⊢ b = a \to (b \in ran (I eval ℤ_{ring}) \leftrightarrow a \in ran (I eval ℤ_{ring}))$
34	13 18 23 26 27 28 29 30 31 32 33	mzpindd	$⊢ (I \in V \land a \in mzPoly (I)) \to a \in ran (I eval ℤ_{ring})$
35		simprlr	$⊢ ((I \in V \land a \in ran (I eval ℤ_{ring})) \land ((x \in ran (I eval ℤ_{ring}) \land x \in mzPoly (I)) \land (y \in ran (I eval ℤ_{ring}) \land y \in mzPoly (I)))) \to x \in mzPoly (I)$
36		simprrr	$⊢ ((I \in V \land a \in ran (I eval ℤ_{ring})) \land ((x \in ran (I eval ℤ_{ring}) \land x \in mzPoly (I)) \land (y \in ran (I eval ℤ_{ring}) \land y \in mzPoly (I)))) \to y \in mzPoly (I)$
37		mzpadd	$⊢ (x \in mzPoly (I) \land y \in mzPoly (I)) \to x +_{f} y \in mzPoly (I)$
38	35 36 37	syl2anc	$⊢ ((I \in V \land a \in ran (I eval ℤ_{ring})) \land ((x \in ran (I eval ℤ_{ring}) \land x \in mzPoly (I)) \land (y \in ran (I eval ℤ_{ring}) \land y \in mzPoly (I)))) \to x +_{f} y \in mzPoly (I)$
39		mzpmul	$⊢ (x \in mzPoly (I) \land y \in mzPoly (I)) \to x \times_{f} y \in mzPoly (I)$
40	35 36 39	syl2anc	$⊢ ((I \in V \land a \in ran (I eval ℤ_{ring})) \land ((x \in ran (I eval ℤ_{ring}) \land x \in mzPoly (I)) \land (y \in ran (I eval ℤ_{ring}) \land y \in mzPoly (I)))) \to x \times_{f} y \in mzPoly (I)$
41		eleq1	$⊢ b = (ℤ^{I}) \times \{x\} \to (b \in mzPoly (I) \leftrightarrow (ℤ^{I}) \times \{x\} \in mzPoly (I))$
42		eleq1	$⊢ b = (y \in (ℤ^{I}) ⟼ y (x)) \to (b \in mzPoly (I) \leftrightarrow (y \in (ℤ^{I}) ⟼ y (x)) \in mzPoly (I))$
43		eleq1	$⊢ b = x \to (b \in mzPoly (I) \leftrightarrow x \in mzPoly (I))$
44		eleq1	$⊢ b = y \to (b \in mzPoly (I) \leftrightarrow y \in mzPoly (I))$
45		eleq1	$⊢ b = x +_{f} y \to (b \in mzPoly (I) \leftrightarrow x +_{f} y \in mzPoly (I))$
46		eleq1	$⊢ b = x \times_{f} y \to (b \in mzPoly (I) \leftrightarrow x \times_{f} y \in mzPoly (I))$
47		eleq1	$⊢ b = a \to (b \in mzPoly (I) \leftrightarrow a \in mzPoly (I))$
48		mzpconst	$⊢ (I \in V \land x \in ℤ) \to (ℤ^{I}) \times \{x\} \in mzPoly (I)$
49	48	adantlr	$⊢ ((I \in V \land a \in ran (I eval ℤ_{ring})) \land x \in ℤ) \to (ℤ^{I}) \times \{x\} \in mzPoly (I)$
50		mzpproj	$⊢ (I \in V \land x \in I) \to (y \in (ℤ^{I}) ⟼ y (x)) \in mzPoly (I)$
51	50	adantlr	$⊢ ((I \in V \land a \in ran (I eval ℤ_{ring})) \land x \in I) \to (y \in (ℤ^{I}) ⟼ y (x)) \in mzPoly (I)$
52		simpr	$⊢ (I \in V \land a \in ran (I eval ℤ_{ring})) \to a \in ran (I eval ℤ_{ring})$
53	1 21 24 4 38 40 41 42 43 44 45 46 47 49 51 52	mpfind	$⊢ (I \in V \land a \in ran (I eval ℤ_{ring})) \to a \in mzPoly (I)$
54	34 53	impbida	$⊢ I \in V \to (a \in mzPoly (I) \leftrightarrow a \in ran (I eval ℤ_{ring}))$
55	54	eqrdv	$⊢ I \in V \to mzPoly (I) = ran (I eval ℤ_{ring})$
56		fvprc	$⊢ \neg I \in V \to mzPoly (I) = \emptyset$
57		df-evl	$⊢ eval = (a \in V, b \in V ⟼ (a evalSub b) ({Base}_{b}))$
58	57	reldmmpo	$⊢ Rel dom eval$
59	58	ovprc1	$⊢ \neg I \in V \to I eval ℤ_{ring} = \emptyset$
60	59	rneqd	$⊢ \neg I \in V \to ran (I eval ℤ_{ring}) = ran \emptyset$
61		rn0	$⊢ ran \emptyset = \emptyset$
62	60 61	eqtrdi	$⊢ \neg I \in V \to ran (I eval ℤ_{ring}) = \emptyset$
63	56 62	eqtr4d	$⊢ \neg I \in V \to mzPoly (I) = ran (I eval ℤ_{ring})$
64	55 63	pm2.61i	$⊢ mzPoly (I) = ran (I eval ℤ_{ring})$

Metamath Proof Explorer

Theorem mzpmfp

Proof