Metamath Proof Explorer

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 snex ⊢ { 𝑓 } ∈ 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 ‘ 𝑉 ) )