---

Step * 1 1 2 of Lemma mul-monomials-ringeq


1. r : CRng
2. f : ℤ ⟶ |r|
3. u : ℤ
4. v : ℤ List
5. ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (ring_term_value(f;imonomial-term(<1, as>)) * \000Cring_term_value(f;imonomial-term(<1, v>))) ∈ |r|)
⊢ ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;[u / v])>)) = (ring_term_value(f;imonomial-term(<1, as>\000C)) * ring_term_value(f;imonomial-term(<1, [u / v]>))) ∈ |r|)
BY
{ (Unfold `merge-int` 0
   THEN Reduce 0
   THEN Fold `merge-int` 0
   THEN (ParallelLast THENA Auto)
   THEN (RWO "imonomial-term-linear-ringeq" 0 THENA Auto)) }

1
1. r : CRng
2. f : ℤ ⟶ |r|
3. u : ℤ
4. v : ℤ List
5. ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (ring_term_value(f;imonomial-term(<1, as>)) * \000Cring_term_value(f;imonomial-term(<1, v>))) ∈ |r|)
6. as : ℤ List
7. ring_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (ring_term_value(f;imonomial-term(<1, as>)) * ring_term_val\000Cue(f;imonomial-term(<1, v>))) ∈ |r|
⊢ (int-to-ring(r;1) * ring_term_value(f;imonomial-term(<1, insert-int(u;merge-int(as;v))>)))
= ((int-to-ring(r;1) * ring_term_value(f;imonomial-term(<1, as>))) * (int-to-ring(r;1) * ring_term_value(f;imonomial-ter\000Cm(<1, [u / v]>))))
∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  f  :  \mBbbZ{}  {}\mrightarrow{}  |r|
3.  u  :  \mBbbZ{}
4.  v  :  \mBbbZ{}  List
5.  \mforall{}as:\mBbbZ{}  List.  (ring\_term\_value(f;imonomial-term(ə,  merge-int(as;v)>))  =  (ring\_term\_value(f;imonomi\000Cal-term(ə,  as>))  *  ring\_term\_value(f;imonomial-term(ə,  v>))))
\mvdash{}  \mforall{}as:\mBbbZ{}  List.  (ring\_term\_value(f;imonomial-term(ə,  merge-int(as;[u  /  v])>))  =  (ring\_term\_value(f;im\000Conomial-term(ə,  as>))  *  ring\_term\_value(f;imonomial-term(ə,  [u  /  v]>))))


By

---

Latex:
(Unfold  `merge-int`  0
  THEN  Reduce  0
  THEN  Fold  `merge-int`  0
  THEN  (ParallelLast  THENA  Auto)
  THEN  (RWO  "imonomial-term-linear-ringeq"  0  THENA  Auto))

---

Home Index