# Metamath Proof Explorer

## Theorem 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 ${⊢}\mathrm{mzPoly}\left({I}\right)=\mathrm{ran}\left({I}\mathrm{eval}{ℤ}_{\mathrm{ring}}\right)$

### Proof

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