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 ↦ ∩ ( mzPolyCld ‘ 𝑣 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmzp	⊢ mzPoly
1		vv	⊢ 𝑣
2		cvv	⊢ V
3		cmzpcl	⊢ mzPolyCld
4	1	cv	⊢ 𝑣
5	4 3	cfv	⊢ ( mzPolyCld ‘ 𝑣 )
6	5	cint	⊢ ∩ ( mzPolyCld ‘ 𝑣 )
7	1 2 6	cmpt	⊢ ( 𝑣 ∈ V ↦ ∩ ( mzPolyCld ‘ 𝑣 ) )
8	0 7	wceq	⊢ mzPoly = ( 𝑣 ∈ V ↦ ∩ ( mzPolyCld ‘ 𝑣 ) )