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 ffvelrn ( ( 𝑔 : 𝑣 ⟶ ℤ ∧ 𝑓𝑣 ) → ( 𝑔𝑓 ) ∈ ℤ )
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 ‘ 𝑉 ) )