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 ‘ 𝐼 ) = ran ( 𝐼 eval ℤring )

Proof

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