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	|- mzPoly = ( v e. _V |-> |^| ( mzPolyCld ` v ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmzp	|- mzPoly
1		vv	|- v
2		cvv	|- _V
3		cmzpcl	|- mzPolyCld
4	1	cv	|- v
5	4 3	cfv	|- ( mzPolyCld ` v )
6	5	cint	|- |^| ( mzPolyCld ` v )
7	1 2 6	cmpt	|- ( v e. _V |-> |^| ( mzPolyCld ` v ) )
8	0 7	wceq	|- mzPoly = ( v e. _V |-> |^| ( mzPolyCld ` v ) )