Definition df-mzp

Description: Polynomials over ZZ with an arbitrary index set, that is, the smallest ring of functions containing all constant functions and all projections. This is almost the most general reasonable definition; to reach full generality, we would need to be able to replace ZZ with an arbitrary (semi)ring (and a coordinate subring), but rings have not been defined yet. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	df-mzp	$$⊢\mathrm{mzPoly}=\left(v\in \mathrm{V}⟼\bigcap \mathrm{mzPolyCld}\left(v\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmzp	$$class\mathrm{mzPoly}$$
1		vv	$$setvarv$$
2		cvv	$$class\mathrm{V}$$
3		cmzpcl	$$class\mathrm{mzPolyCld}$$
4	1	cv	$$setvarv$$
5	4 3	cfv	$$class\mathrm{mzPolyCld}\left(v\right)$$
6	5	cint	$$class\bigcap \mathrm{mzPolyCld}\left(v\right)$$
7	1 2 6	cmpt	$$class\left(v\in \mathrm{V}⟼\bigcap \mathrm{mzPolyCld}\left(v\right)\right)$$
8	0 7	wceq	$$wff\mathrm{mzPoly}=\left(v\in \mathrm{V}⟼\bigcap \mathrm{mzPolyCld}\left(v\right)\right)$$