Definition df-mzpcl

Description: Define the polynomially closed function rings over an arbitrary index set v . The set ( mzPolyCldv ) contains all sets of functions from ( ZZ ^m v ) to ZZ which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself ( mzPolyv ) ; see df-mzp . (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	df-mzpcl	⊢ mzPolyCld = ( 𝑣 ∈ V ↦ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmzpcl	⊢ mzPolyCld
1		vv	⊢ 𝑣
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		cz	⊢ ℤ
5		cmap	⊢ ↑m
6	1	cv	⊢ 𝑣
7	4 6 5	co	⊢ ( ℤ ↑m 𝑣 )
8	4 7 5	co	⊢ ( ℤ ↑m ( ℤ ↑m 𝑣 ) )
9	8	cpw	⊢ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) )
10		vi	⊢ 𝑖
11	10	cv	⊢ 𝑖
12	11	csn	⊢ { 𝑖 }
13	7 12	cxp	⊢ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } )
14	3	cv	⊢ 𝑝
15	13 14	wcel	⊢ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝
16	15 10 4	wral	⊢ ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝
17		vj	⊢ 𝑗
18		vx	⊢ 𝑥
19	18	cv	⊢ 𝑥
20	17	cv	⊢ 𝑗
21	20 19	cfv	⊢ ( 𝑥 ‘ 𝑗 )
22	18 7 21	cmpt	⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) )
23	22 14	wcel	⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝
24	23 17 6	wral	⊢ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝
25	16 24	wa	⊢ ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 )
26		vf	⊢ 𝑓
27		vg	⊢ 𝑔
28	26	cv	⊢ 𝑓
29		caddc	⊢ +
30	29	cof	⊢ ∘f +
31	27	cv	⊢ 𝑔
32	28 31 30	co	⊢ ( 𝑓 ∘f + 𝑔 )
33	32 14	wcel	⊢ ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝
34		cmul	⊢ ·
35	34	cof	⊢ ∘f ·
36	28 31 35	co	⊢ ( 𝑓 ∘f · 𝑔 )
37	36 14	wcel	⊢ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝
38	33 37	wa	⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 )
39	38 27 14	wral	⊢ ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 )
40	39 26 14	wral	⊢ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 )
41	25 40	wa	⊢ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) )
42	41 3 9	crab	⊢ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) }
43	1 2 42	cmpt	⊢ ( 𝑣 ∈ V ↦ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )
44	0 43	wceq	⊢ mzPolyCld = ( 𝑣 ∈ V ↦ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑣 ( 𝑥 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )