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 e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( v = V -> ( ZZ ^m v ) = ( ZZ ^m V ) )
2 1 oveq2d 
 |-  ( v = V -> ( ZZ ^m ( ZZ ^m v ) ) = ( ZZ ^m ( ZZ ^m V ) ) )
3 fveq2 
 |-  ( v = V -> ( mzPolyCld ` v ) = ( mzPolyCld ` V ) )
4 2 3 eleq12d 
 |-  ( v = V -> ( ( ZZ ^m ( ZZ ^m v ) ) e. ( mzPolyCld ` v ) <-> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) ) )
5 ssid 
 |-  ( ZZ ^m ( ZZ ^m v ) ) C_ ( ZZ ^m ( ZZ ^m v ) )
6 ovex 
 |-  ( ZZ ^m v ) e. _V
7 zex 
 |-  ZZ e. _V
8 6 7 constmap 
 |-  ( f e. ZZ -> ( ( ZZ ^m v ) X. { f } ) e. ( ZZ ^m ( ZZ ^m v ) ) )
9 8 rgen 
 |-  A. f e. ZZ ( ( ZZ ^m v ) X. { f } ) e. ( ZZ ^m ( ZZ ^m v ) )
10 vex 
 |-  v e. _V
11 7 10 elmap 
 |-  ( g e. ( ZZ ^m v ) <-> g : v --> ZZ )
12 ffvelrn 
 |-  ( ( g : v --> ZZ /\ f e. v ) -> ( g ` f ) e. ZZ )
13 11 12 sylanb 
 |-  ( ( g e. ( ZZ ^m v ) /\ f e. v ) -> ( g ` f ) e. ZZ )
14 13 ancoms 
 |-  ( ( f e. v /\ g e. ( ZZ ^m v ) ) -> ( g ` f ) e. ZZ )
15 14 fmpttd 
 |-  ( f e. v -> ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) : ( ZZ ^m v ) --> ZZ )
16 7 6 elmap 
 |-  ( ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) ) <-> ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) : ( ZZ ^m v ) --> ZZ )
17 15 16 sylibr 
 |-  ( f e. v -> ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) ) )
18 17 rgen 
 |-  A. f e. v ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) )
19 9 18 pm3.2i 
 |-  ( A. f e. ZZ ( ( ZZ ^m v ) X. { f } ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ A. f e. v ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) ) )
20 zaddcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
21 20 adantl 
 |-  ( ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + b ) e. ZZ )
22 simpl 
 |-  ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) -> f : ( ZZ ^m v ) --> ZZ )
23 simpr 
 |-  ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) -> g : ( ZZ ^m v ) --> ZZ )
24 ovexd 
 |-  ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) -> ( ZZ ^m v ) e. _V )
25 inidm 
 |-  ( ( ZZ ^m v ) i^i ( ZZ ^m v ) ) = ( ZZ ^m v )
26 21 22 23 24 24 25 off 
 |-  ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) -> ( f oF + g ) : ( ZZ ^m v ) --> ZZ )
27 zmulcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ )
28 27 adantl 
 |-  ( ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a x. b ) e. ZZ )
29 28 22 23 24 24 25 off 
 |-  ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) -> ( f oF x. g ) : ( ZZ ^m v ) --> ZZ )
30 26 29 jca 
 |-  ( ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) -> ( ( f oF + g ) : ( ZZ ^m v ) --> ZZ /\ ( f oF x. g ) : ( ZZ ^m v ) --> ZZ ) )
31 7 6 elmap 
 |-  ( f e. ( ZZ ^m ( ZZ ^m v ) ) <-> f : ( ZZ ^m v ) --> ZZ )
32 7 6 elmap 
 |-  ( g e. ( ZZ ^m ( ZZ ^m v ) ) <-> g : ( ZZ ^m v ) --> ZZ )
33 31 32 anbi12i 
 |-  ( ( f e. ( ZZ ^m ( ZZ ^m v ) ) /\ g e. ( ZZ ^m ( ZZ ^m v ) ) ) <-> ( f : ( ZZ ^m v ) --> ZZ /\ g : ( ZZ ^m v ) --> ZZ ) )
34 7 6 elmap 
 |-  ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) <-> ( f oF + g ) : ( ZZ ^m v ) --> ZZ )
35 7 6 elmap 
 |-  ( ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) <-> ( f oF x. g ) : ( ZZ ^m v ) --> ZZ )
36 34 35 anbi12i 
 |-  ( ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) ) <-> ( ( f oF + g ) : ( ZZ ^m v ) --> ZZ /\ ( f oF x. g ) : ( ZZ ^m v ) --> ZZ ) )
37 30 33 36 3imtr4i 
 |-  ( ( f e. ( ZZ ^m ( ZZ ^m v ) ) /\ g e. ( ZZ ^m ( ZZ ^m v ) ) ) -> ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) ) )
38 37 rgen2 
 |-  A. f e. ( ZZ ^m ( ZZ ^m v ) ) A. g e. ( ZZ ^m ( ZZ ^m v ) ) ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) )
39 19 38 pm3.2i 
 |-  ( ( A. f e. ZZ ( ( ZZ ^m v ) X. { f } ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ A. f e. v ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) ) ) /\ A. f e. ( ZZ ^m ( ZZ ^m v ) ) A. g e. ( ZZ ^m ( ZZ ^m v ) ) ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) ) )
40 elmzpcl 
 |-  ( v e. _V -> ( ( ZZ ^m ( ZZ ^m v ) ) e. ( mzPolyCld ` v ) <-> ( ( ZZ ^m ( ZZ ^m v ) ) C_ ( ZZ ^m ( ZZ ^m v ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m v ) X. { f } ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ A. f e. v ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) ) ) /\ A. f e. ( ZZ ^m ( ZZ ^m v ) ) A. g e. ( ZZ ^m ( ZZ ^m v ) ) ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) ) ) ) ) )
41 10 40 ax-mp 
 |-  ( ( ZZ ^m ( ZZ ^m v ) ) e. ( mzPolyCld ` v ) <-> ( ( ZZ ^m ( ZZ ^m v ) ) C_ ( ZZ ^m ( ZZ ^m v ) ) /\ ( ( A. f e. ZZ ( ( ZZ ^m v ) X. { f } ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ A. f e. v ( g e. ( ZZ ^m v ) |-> ( g ` f ) ) e. ( ZZ ^m ( ZZ ^m v ) ) ) /\ A. f e. ( ZZ ^m ( ZZ ^m v ) ) A. g e. ( ZZ ^m ( ZZ ^m v ) ) ( ( f oF + g ) e. ( ZZ ^m ( ZZ ^m v ) ) /\ ( f oF x. g ) e. ( ZZ ^m ( ZZ ^m v ) ) ) ) ) )
42 5 39 41 mpbir2an 
 |-  ( ZZ ^m ( ZZ ^m v ) ) e. ( mzPolyCld ` v )
43 4 42 vtoclg 
 |-  ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) )