Theorem mzpincl

Description: Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	mzpincl	⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mzpval	⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) = ∩ ( mzPolyCld ‘ 𝑉 ) )
2		mzpclall	⊢ ( 𝑉 ∈ V → ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) )
3		intss1	⊢ ( ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) → ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
4	2 3	syl	⊢ ( 𝑉 ∈ V → ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
5		simpr	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑓 ∈ ℤ ) ∧ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ) → 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) )
6		simplr	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑓 ∈ ℤ ) ∧ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ) → 𝑓 ∈ ℤ )
7		mzpcl1	⊢ ( ( 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝑓 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑎 )
8	5 6 7	syl2anc	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑓 ∈ ℤ ) ∧ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ) → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑎 )
9	8	ralrimiva	⊢ ( ( 𝑉 ∈ V ∧ 𝑓 ∈ ℤ ) → ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑎 )
10		ovex	⊢ ( ℤ ↑m 𝑉 ) ∈ V
11		vsnex	⊢ { 𝑓 } ∈ V
12	10 11	xpex	⊢ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ V
13	12	elint2	⊢ ( ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ↔ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑎 )
14	9 13	sylibr	⊢ ( ( 𝑉 ∈ V ∧ 𝑓 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) )
15	14	ralrimiva	⊢ ( 𝑉 ∈ V → ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) )
16		simpr	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ) → 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) )
17		simplr	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ) → 𝑓 ∈ 𝑉 )
18		mzpcl2	⊢ ( ( 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝑓 ∈ 𝑉 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑎 )
19	16 17 18	syl2anc	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑎 )
20	19	ralrimiva	⊢ ( ( 𝑉 ∈ V ∧ 𝑓 ∈ 𝑉 ) → ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑎 )
21	10	mptex	⊢ ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ V
22	21	elint2	⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ↔ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑎 )
23	20 22	sylibr	⊢ ( ( 𝑉 ∈ V ∧ 𝑓 ∈ 𝑉 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) )
24	23	ralrimiva	⊢ ( 𝑉 ∈ V → ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) )
25	15 24	jca	⊢ ( 𝑉 ∈ V → ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) )
26		vex	⊢ 𝑓 ∈ V
27	26	elint2	⊢ ( 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ↔ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) 𝑓 ∈ 𝑎 )
28		vex	⊢ 𝑔 ∈ V
29	28	elint2	⊢ ( 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ↔ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) 𝑔 ∈ 𝑎 )
30		mzpcl34	⊢ ( ( 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎 ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) )
31	30	3expib	⊢ ( 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) → ( ( 𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎 ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) ) )
32	31	ralimia	⊢ ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎 ) → ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) )
33		r19.26	⊢ ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎 ) ↔ ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) 𝑓 ∈ 𝑎 ∧ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) 𝑔 ∈ 𝑎 ) )
34		r19.26	⊢ ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) ↔ ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) )
35	32 33 34	3imtr3i	⊢ ( ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) 𝑓 ∈ 𝑎 ∧ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) 𝑔 ∈ 𝑎 ) → ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) )
36	27 29 35	syl2anb	⊢ ( ( 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) → ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) )
37		ovex	⊢ ( 𝑓 ∘f + 𝑔 ) ∈ V
38	37	elint2	⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ↔ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 )
39		ovex	⊢ ( 𝑓 ∘f · 𝑔 ) ∈ V
40	39	elint2	⊢ ( ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ↔ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 )
41	38 40	anbi12i	⊢ ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) ↔ ( ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f + 𝑔 ) ∈ 𝑎 ∧ ∀ 𝑎 ∈ ( mzPolyCld ‘ 𝑉 ) ( 𝑓 ∘f · 𝑔 ) ∈ 𝑎 ) )
42	36 41	sylibr	⊢ ( ( 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) )
43	42	a1i	⊢ ( 𝑉 ∈ V → ( ( 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) ) )
44	43	ralrimivv	⊢ ( 𝑉 ∈ V → ∀ 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∀ 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) )
45	4 25 44	jca32	⊢ ( 𝑉 ∈ V → ( ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) ∧ ∀ 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∀ 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) ) ) )
46		elmzpcl	⊢ ( 𝑉 ∈ V → ( ∩ ( mzPolyCld ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) ∧ ∀ 𝑓 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∀ 𝑔 ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ∩ ( mzPolyCld ‘ 𝑉 ) ) ) ) ) )
47	45 46	mpbird	⊢ ( 𝑉 ∈ V → ∩ ( mzPolyCld ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) )
48	1 47	eqeltrd	⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) )