Metamath Proof Explorer

Theorem mzpclall

Description: The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpclall ( 𝑉 ∈ V → ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑣 = 𝑉 → ( ℤ ↑m 𝑣 ) = ( ℤ ↑m 𝑉 ) )
2 1 oveq2d ⊢ ( 𝑣 = 𝑉 → ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) = ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
3 fveq2 ⊢ ( 𝑣 = 𝑉 → ( mzPolyCld ‘ 𝑣 ) = ( mzPolyCld ‘ 𝑉 ) )
4 2 3 eleq12d ⊢ ( 𝑣 = 𝑉 → ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) ↔ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) ) )
5 ssid ⊢ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑣 ) )
6 ovex ⊢ ( ℤ ↑m 𝑣 ) ∈ V
7 zex ⊢ ℤ ∈ V
8 6 7 constmap ⊢ ( 𝑓 ∈ ℤ → ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) )
9 8 rgen ⊢ ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) )
10 vex ⊢ 𝑣 ∈ V
11 7 10 elmap ⊢ ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↔ 𝑔 : 𝑣 ⟶ ℤ )
12 ffvelcdm ⊢ ( ( 𝑔 : 𝑣 ⟶ ℤ ∧ 𝑓 ∈ 𝑣 ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ )
13 11 12 sylanb ⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ∧ 𝑓 ∈ 𝑣 ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ )
14 13 ancoms ⊢ ( ( 𝑓 ∈ 𝑣 ∧ 𝑔 ∈ ( ℤ ↑m 𝑣 ) ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ )
15 14 fmpttd ⊢ ( 𝑓 ∈ 𝑣 → ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
16 7 6 elmap ⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
17 15 16 sylibr ⊢ ( 𝑓 ∈ 𝑣 → ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) )
18 17 rgen ⊢ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) )
19 9 18 pm3.2i ⊢ ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) )
20 zaddcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
21 20 adantl ⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
22 simpl ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
23 simpr ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
24 ovexd ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( ℤ ↑m 𝑣 ) ∈ V )
25 inidm ⊢ ( ( ℤ ↑m 𝑣 ) ∩ ( ℤ ↑m 𝑣 ) ) = ( ℤ ↑m 𝑣 )
26 21 22 23 24 24 25 off ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
27 zmulcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
28 27 adantl ⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
29 28 22 23 24 24 25 off ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
30 26 29 jca ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) )
31 7 6 elmap ⊢ ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
32 7 6 elmap ⊢ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
33 31 32 anbi12i ⊢ ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ↔ ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) )
34 7 6 elmap ⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
35 7 6 elmap ⊢ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ )
36 34 35 anbi12i ⊢ ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ↔ ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) )
37 30 33 36 3imtr4i ⊢ ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) )
38 37 rgen2 ⊢ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) )
39 19 38 pm3.2i ⊢ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ∧ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) )
40 elmzpcl ⊢ ( 𝑣 ∈ V → ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) ↔ ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ∧ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ) ) ) )
41 10 40 ax-mp ⊢ ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) ↔ ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ∧ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ) ) )
42 5 39 41 mpbir2an ⊢ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 )
43 4 42 vtoclg ⊢ ( 𝑉 ∈ V → ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) )