Metamath Proof Explorer

Theorem mzpmfp

Description: Relationship between multivariate Z-polynomials and general multivariate polynomial functions. (Contributed by Stefan O'Rear, 20-Mar-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Assertion mzpmfp 
|- ( mzPoly ` I ) = ran ( I eval ZZring )

Proof

Step Hyp Ref Expression
1 zringbas 
 |-  ZZ = ( Base ` ZZring )
2 eqid 
 |-  ( I eval ZZring ) = ( I eval ZZring )
3 2 1 evlval 
 |-  ( I eval ZZring ) = ( ( I evalSub ZZring ) ` ZZ )
4 3 rneqi 
 |-  ran ( I eval ZZring ) = ran ( ( I evalSub ZZring ) ` ZZ )
5 simpl 
 |-  ( ( I e. _V /\ f e. ZZ ) -> I e. _V )
6 zringcrng 
 |-  ZZring e. CRing
7 6 a1i 
 |-  ( ( I e. _V /\ f e. ZZ ) -> ZZring e. CRing )
8 zringring 
 |-  ZZring e. Ring
9 1 subrgid 
 |-  ( ZZring e. Ring -> ZZ e. ( SubRing ` ZZring ) )
10 8 9 ax-mp 
 |-  ZZ e. ( SubRing ` ZZring )
11 10 a1i 
 |-  ( ( I e. _V /\ f e. ZZ ) -> ZZ e. ( SubRing ` ZZring ) )
12 simpr 
 |-  ( ( I e. _V /\ f e. ZZ ) -> f e. ZZ )
13 1 4 5 7 11 12 mpfconst 
 |-  ( ( I e. _V /\ f e. ZZ ) -> ( ( ZZ ^m I ) X. { f } ) e. ran ( I eval ZZring ) )
14 simpl 
 |-  ( ( I e. _V /\ f e. I ) -> I e. _V )
15 6 a1i 
 |-  ( ( I e. _V /\ f e. I ) -> ZZring e. CRing )
16 10 a1i 
 |-  ( ( I e. _V /\ f e. I ) -> ZZ e. ( SubRing ` ZZring ) )
17 simpr 
 |-  ( ( I e. _V /\ f e. I ) -> f e. I )
18 1 4 14 15 16 17 mpfproj 
 |-  ( ( I e. _V /\ f e. I ) -> ( g e. ( ZZ ^m I ) |-> ( g ` f ) ) e. ran ( I eval ZZring ) )
19 simp2r 
 |-  ( ( I e. _V /\ ( f : ( ZZ ^m I ) --> ZZ /\ f e. ran ( I eval ZZring ) ) /\ ( g : ( ZZ ^m I ) --> ZZ /\ g e. ran ( I eval ZZring ) ) ) -> f e. ran ( I eval ZZring ) )
20 simp3r 
 |-  ( ( I e. _V /\ ( f : ( ZZ ^m I ) --> ZZ /\ f e. ran ( I eval ZZring ) ) /\ ( g : ( ZZ ^m I ) --> ZZ /\ g e. ran ( I eval ZZring ) ) ) -> g e. ran ( I eval ZZring ) )
21 zringplusg 
 |-  + = ( +g ` ZZring )
22 4 21 mpfaddcl 
 |-  ( ( f e. ran ( I eval ZZring ) /\ g e. ran ( I eval ZZring ) ) -> ( f oF + g ) e. ran ( I eval ZZring ) )
23 19 20 22 syl2anc 
 |-  ( ( I e. _V /\ ( f : ( ZZ ^m I ) --> ZZ /\ f e. ran ( I eval ZZring ) ) /\ ( g : ( ZZ ^m I ) --> ZZ /\ g e. ran ( I eval ZZring ) ) ) -> ( f oF + g ) e. ran ( I eval ZZring ) )
24 zringmulr 
 |-  x. = ( .r ` ZZring )
25 4 24 mpfmulcl 
 |-  ( ( f e. ran ( I eval ZZring ) /\ g e. ran ( I eval ZZring ) ) -> ( f oF x. g ) e. ran ( I eval ZZring ) )
26 19 20 25 syl2anc 
 |-  ( ( I e. _V /\ ( f : ( ZZ ^m I ) --> ZZ /\ f e. ran ( I eval ZZring ) ) /\ ( g : ( ZZ ^m I ) --> ZZ /\ g e. ran ( I eval ZZring ) ) ) -> ( f oF x. g ) e. ran ( I eval ZZring ) )
27 eleq1 
 |-  ( b = ( ( ZZ ^m I ) X. { f } ) -> ( b e. ran ( I eval ZZring ) <-> ( ( ZZ ^m I ) X. { f } ) e. ran ( I eval ZZring ) ) )
28 eleq1 
 |-  ( b = ( g e. ( ZZ ^m I ) |-> ( g ` f ) ) -> ( b e. ran ( I eval ZZring ) <-> ( g e. ( ZZ ^m I ) |-> ( g ` f ) ) e. ran ( I eval ZZring ) ) )
29 eleq1 
 |-  ( b = f -> ( b e. ran ( I eval ZZring ) <-> f e. ran ( I eval ZZring ) ) )
30 eleq1 
 |-  ( b = g -> ( b e. ran ( I eval ZZring ) <-> g e. ran ( I eval ZZring ) ) )
31 eleq1 
 |-  ( b = ( f oF + g ) -> ( b e. ran ( I eval ZZring ) <-> ( f oF + g ) e. ran ( I eval ZZring ) ) )
32 eleq1 
 |-  ( b = ( f oF x. g ) -> ( b e. ran ( I eval ZZring ) <-> ( f oF x. g ) e. ran ( I eval ZZring ) ) )
33 eleq1 
 |-  ( b = a -> ( b e. ran ( I eval ZZring ) <-> a e. ran ( I eval ZZring ) ) )
34 13 18 23 26 27 28 29 30 31 32 33 mzpindd 
 |-  ( ( I e. _V /\ a e. ( mzPoly ` I ) ) -> a e. ran ( I eval ZZring ) )
35 simprlr 
 |-  ( ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) /\ ( ( x e. ran ( I eval ZZring ) /\ x e. ( mzPoly ` I ) ) /\ ( y e. ran ( I eval ZZring ) /\ y e. ( mzPoly ` I ) ) ) ) -> x e. ( mzPoly ` I ) )
36 simprrr 
 |-  ( ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) /\ ( ( x e. ran ( I eval ZZring ) /\ x e. ( mzPoly ` I ) ) /\ ( y e. ran ( I eval ZZring ) /\ y e. ( mzPoly ` I ) ) ) ) -> y e. ( mzPoly ` I ) )
37 mzpadd 
 |-  ( ( x e. ( mzPoly ` I ) /\ y e. ( mzPoly ` I ) ) -> ( x oF + y ) e. ( mzPoly ` I ) )
38 35 36 37 syl2anc 
 |-  ( ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) /\ ( ( x e. ran ( I eval ZZring ) /\ x e. ( mzPoly ` I ) ) /\ ( y e. ran ( I eval ZZring ) /\ y e. ( mzPoly ` I ) ) ) ) -> ( x oF + y ) e. ( mzPoly ` I ) )
39 mzpmul 
 |-  ( ( x e. ( mzPoly ` I ) /\ y e. ( mzPoly ` I ) ) -> ( x oF x. y ) e. ( mzPoly ` I ) )
40 35 36 39 syl2anc 
 |-  ( ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) /\ ( ( x e. ran ( I eval ZZring ) /\ x e. ( mzPoly ` I ) ) /\ ( y e. ran ( I eval ZZring ) /\ y e. ( mzPoly ` I ) ) ) ) -> ( x oF x. y ) e. ( mzPoly ` I ) )
41 eleq1 
 |-  ( b = ( ( ZZ ^m I ) X. { x } ) -> ( b e. ( mzPoly ` I ) <-> ( ( ZZ ^m I ) X. { x } ) e. ( mzPoly ` I ) ) )
42 eleq1 
 |-  ( b = ( y e. ( ZZ ^m I ) |-> ( y ` x ) ) -> ( b e. ( mzPoly ` I ) <-> ( y e. ( ZZ ^m I ) |-> ( y ` x ) ) e. ( mzPoly ` I ) ) )
43 eleq1 
 |-  ( b = x -> ( b e. ( mzPoly ` I ) <-> x e. ( mzPoly ` I ) ) )
44 eleq1 
 |-  ( b = y -> ( b e. ( mzPoly ` I ) <-> y e. ( mzPoly ` I ) ) )
45 eleq1 
 |-  ( b = ( x oF + y ) -> ( b e. ( mzPoly ` I ) <-> ( x oF + y ) e. ( mzPoly ` I ) ) )
46 eleq1 
 |-  ( b = ( x oF x. y ) -> ( b e. ( mzPoly ` I ) <-> ( x oF x. y ) e. ( mzPoly ` I ) ) )
47 eleq1 
 |-  ( b = a -> ( b e. ( mzPoly ` I ) <-> a e. ( mzPoly ` I ) ) )
48 mzpconst 
 |-  ( ( I e. _V /\ x e. ZZ ) -> ( ( ZZ ^m I ) X. { x } ) e. ( mzPoly ` I ) )
49 48 adantlr 
 |-  ( ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) /\ x e. ZZ ) -> ( ( ZZ ^m I ) X. { x } ) e. ( mzPoly ` I ) )
50 mzpproj 
 |-  ( ( I e. _V /\ x e. I ) -> ( y e. ( ZZ ^m I ) |-> ( y ` x ) ) e. ( mzPoly ` I ) )
51 50 adantlr 
 |-  ( ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) /\ x e. I ) -> ( y e. ( ZZ ^m I ) |-> ( y ` x ) ) e. ( mzPoly ` I ) )
52 simpr 
 |-  ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) -> a e. ran ( I eval ZZring ) )
53 1 21 24 4 38 40 41 42 43 44 45 46 47 49 51 52 mpfind 
 |-  ( ( I e. _V /\ a e. ran ( I eval ZZring ) ) -> a e. ( mzPoly ` I ) )
54 34 53 impbida 
 |-  ( I e. _V -> ( a e. ( mzPoly ` I ) <-> a e. ran ( I eval ZZring ) ) )
55 54 eqrdv 
 |-  ( I e. _V -> ( mzPoly ` I ) = ran ( I eval ZZring ) )
56 fvprc 
 |-  ( -. I e. _V -> ( mzPoly ` I ) = (/) )
57 df-evl 
 |-  eval = ( a e. _V , b e. _V |-> ( ( a evalSub b ) ` ( Base ` b ) ) )
58 57 reldmmpo 
 |-  Rel dom eval
59 58 ovprc1 
 |-  ( -. I e. _V -> ( I eval ZZring ) = (/) )
60 59 rneqd 
 |-  ( -. I e. _V -> ran ( I eval ZZring ) = ran (/) )
61 rn0 
 |-  ran (/) = (/)
62 60 61 eqtrdi 
 |-  ( -. I e. _V -> ran ( I eval ZZring ) = (/) )
63 56 62 eqtr4d 
 |-  ( -. I e. _V -> ( mzPoly ` I ) = ran ( I eval ZZring ) )
64 55 63 pm2.61i 
 |-  ( mzPoly ` I ) = ran ( I eval ZZring )