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 ring

Proof

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